From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 17:38:47 +0000 (+0000) Subject: Dummy dependent products in inductive types arities are no longer cleaned. X-Git-Tag: make_still_working~5170 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ef3dfcdad5cd42f31ce5575aa1d03247d4547b38;p=helm.git Dummy dependent products in inductive types arities are no longer cleaned. --- diff --git a/helm/software/matita/library/algebra/CoRN/Setoids.ma b/helm/software/matita/library/algebra/CoRN/Setoids.ma index ddbb807a8..3b37dc42b 100644 --- a/helm/software/matita/library/algebra/CoRN/Setoids.ma +++ b/helm/software/matita/library/algebra/CoRN/Setoids.ma @@ -237,8 +237,8 @@ apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B)) unfold prod_ap. simplify. intros. elim H - [apply (ap_irreflexive A t H1) - |apply (ap_irreflexive B t1 H1) + [apply (ap_irreflexive A a H1) + |apply (ap_irreflexive B b H1) ] |unfold. intros 2. @@ -258,14 +258,14 @@ apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B)) unfold prod_ap in H. simplify in H. unfold prod_ap. simplify. elim H - [cut ((t \neq t4) \or (t4 \neq t2)) + [cut ((a \neq a2) \or (a2 \neq a1)) [elim Hcut [left. left. assumption |right. left. assumption ] |apply (ap_cotransitive A). assumption ] - |cut ((t1 \neq t5) \or (t5 \neq t3)) + |cut ((b \neq b2) \or (b2 \neq b1)) [elim Hcut [left. right. assumption |right. right. assumption @@ -291,8 +291,8 @@ apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B)) |intro. unfold. intro. elim H. elim H1 - [apply (eq_imp_not_ap A t t2 H2). assumption - |apply (eq_imp_not_ap B t1 t3 H3). assumption + [apply (eq_imp_not_ap A a a1 H2). assumption + |apply (eq_imp_not_ap B b b1 H3). assumption ] ] ]