qed.
(* Piu' semplice e non lascia l'ipotesi inutile Hcut *)
alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
theorem test_inversion2: \forall n. le n O \to n=O.
intros.
qed.
(* Piu' semplice e non lascia l'ipotesi inutile Hcut *)
alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
theorem test_inversion2: \forall n. le n O \to n=O.
intros.