From f110058b4445285a17447ca46211259349764c84 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 16 Nov 2011 15:15:13 +0000 Subject: [PATCH] inversion replaced by elim (???) --- matita/matita/lib/basics/star.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma index c1b9c77c0..d17dcca7e 100644 --- a/matita/matita/lib/basics/star.ma +++ b/matita/matita/lib/basics/star.ma @@ -107,7 +107,7 @@ inductive equiv (A:Type[0]) (R:relation A) : A → A → Prop ≝ theorem trans_equiv: ∀A,R,a,b,c. equiv A R a b → equiv A R b c → equiv A R a c. -#A #R #a #b #c #Hab #Hbc (inversion Hbc) /2/ +#A #R #a #b #c #Hab #Hbc (elim Hbc) /2/ qed. theorem equiv_equiv: ∀A,R. exteqR … (equiv A R) (equiv A (equiv A R)). -- 2.39.5