From 3cfa031bcd0620b3662b907cbbf07c65d7e96636 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 13 May 2009 09:55:04 +0000 Subject: [PATCH] Via un'altra linea... --- .../software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma index be3033199..14f1525a7 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma @@ -50,7 +50,7 @@ lemma JSubtype_inv: intros; generalize in match (refl_eq ? T); generalize in match (refl_eq ? G); - elim H5 in ⊢ (? ? ? % → ? ? ? % → %); destruct; autobatch depth=3 width=4 size=7; + elim H5 in ⊢ (? ? ? % → ? ? ? % → %); destruct; autobatch width=4 size=7; qed. theorem narrowing:∀X,G,G1,U,P,M,N. -- 2.39.2