From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 19:14:34 +0000 (+0000) Subject: Dummy dependent types are no longer cleaned in inductive type arities. X-Git-Tag: make_still_working~5159 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8c0bf2ae3a055c2962014bc92e70205ccf127335;p=helm.git Dummy dependent types are no longer cleaned in inductive type arities. --- diff --git a/helm/software/matita/library/list/sort.ma b/helm/software/matita/library/list/sort.ma index c67b28227..857ab4e86 100644 --- a/helm/software/matita/library/list/sort.ma +++ b/helm/software/matita/library/list/sort.ma @@ -151,12 +151,12 @@ lemma ordered_injective: clear H1; elim l1; [ simplify; reflexivity; - | cut ((le t t1 \land ordered A le (t1::l2)) = true); + | cut ((le a a1 \land ordered A le (a1::l2)) = true); [ generalize in match Hcut; apply andb_elim; - elim (le t t1); + elim (le a a1); [ simplify; - fold simplify (ordered ? le (t1::l2)); + fold simplify (ordered ? le (a1::l2)); intros; assumption; | simplify; intros (Habsurd); @@ -185,7 +185,7 @@ lemma insert_sorted: elim l'; simplify; [ rewrite > H5; reflexivity - | elim (le x t); simplify; + | elim (le x a); simplify; [ rewrite > H5; reflexivity | simplify in H4; @@ -212,7 +212,7 @@ theorem insertionsort_sorted: elim l; [ simplify; reflexivity; - | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) t); + | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) a); assumption; ] qed. \ No newline at end of file