intro l1 l2 h
L : Type u
ν : Type v
inst✝³ : LitVar L ν
inst✝² : LawfulLitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
⊢ Function.Injective toPropFun
L : Type u
ν : Type v
inst✝³ : LitVar L ν
inst✝² : LawfulLitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
h : toPropFun l1 = toPropFun l2
⊢ l1 = l2