Open fblanqui opened 2 years ago
Prop:Type. def Prf:Prop -> Type. N:Type. eq:N -> N -> Prop. def add:N -> N -> N. add_com1 (x:N) (y:N) : Prf(eq (add x y) (add y x)). def add_com2 (x:N) (y:N) : Prf(eq (add x y) (add y x)). (; fails ;)