From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 18 May 2008 19:22:55 +0000 (+0000)
Subject: Dummy dependent types are no longer cleaned in inductive type arities.
X-Git-Tag: make_still_working~5158
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b671a48a8cdce63bd7b15af656a75a91463c0e31;p=helm.git

Dummy dependent types are no longer cleaned in inductive type arities.
---

diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
index f68cfd22c..d647830bf 100644
--- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma
+++ b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
@@ -396,7 +396,7 @@ theorem mem_to_exists_l1_l2:
   [ simplify in H1;
     destruct H1
   | simplify in H2;
-    apply (bool_elim ? (eq n t));
+    apply (bool_elim ? (eq n a));
     intro;
      [ apply (ex_intro ? ? []);
        apply (ex_intro ? ? l1);
@@ -408,8 +408,8 @@ theorem mem_to_exists_l1_l2:
        elim (H H1 H2);
        elim H4;
        rewrite > H5;
-       apply (ex_intro ? ? (t::a));
-       apply (ex_intro ? ? a1);
+       apply (ex_intro ? ? (a::a1));
+       apply (ex_intro ? ? a2);
        simplify;
        reflexivity
      ]
@@ -467,7 +467,7 @@ lemma mem_same_atom_to_exists:
   [ simplify in H;
     destruct H
   | simplify in H1;
-    apply (bool_elim ? (same_atom f t));
+    apply (bool_elim ? (same_atom f a));
     intros;
      [ elim (same_atom_to_exists ? ? H2);
        autobatch
@@ -491,14 +491,14 @@ lemma look_for_axiom:
     simplify;
     reflexivity
   | intros;
-    generalize in match (refl_eq ? (mem ? same_atom t l2));
-    elim (mem ? same_atom t l2) in ⊢ (? ? ? %→?);
+    generalize in match (refl_eq ? (mem ? same_atom a l2));
+    elim (mem ? same_atom a l2) in ⊢ (? ? ? %→?);
      [ left;
        elim (mem_to_exists_l1_l2 ? ? ? ? same_atom_to_eq H1);
        elim H2; clear H2;
        elim (mem_same_atom_to_exists ? ? H1);
        rewrite > H2 in H3;
-       apply (ex_intro ? ? a2);
+       apply (ex_intro ? ? a3);
        rewrite > H2;
        apply (ex_intro ? ? []);
        simplify;
@@ -506,22 +506,22 @@ lemma look_for_axiom:
      | elim (H l2);
         [ left;
           decompose;
-          apply (ex_intro ? ? a);
-          apply (ex_intro ? ? (t::a1));
+          apply (ex_intro ? ? a1);
+          apply (ex_intro ? ? (a::a2));
           simplify;
-          apply (ex_intro ? ? a2);
           apply (ex_intro ? ? a3);
+          apply (ex_intro ? ? a4);
           autobatch
         | right;
           intro;
-          apply (bool_elim ? (same_atom t (FAtom n1)));
+          apply (bool_elim ? (same_atom a (FAtom n1)));
            [ intro;
              rewrite > (eq_to_eq_mem ? ? transitiveb_same_atom ? ? ? H3) in H1;
              rewrite > H1;
              autobatch
            | intro;
              change in ⊢ (? ? (? % ?) ?) with
-              (match same_atom (FAtom n1) t with
+              (match same_atom (FAtom n1) a with
                 [true ⇒ true
                 |false ⇒ mem ? same_atom (FAtom n1) l
                 ]);
@@ -603,7 +603,7 @@ lemma sizel_0_no_axiom_is_tautology:
        destruct H2
      | simplify;
        intro;
-       elim t;
+       elim a;
         [ right;
           apply (ex_intro ? ? []);
           simplify;
@@ -616,10 +616,10 @@ lemma sizel_0_no_axiom_is_tautology:
              elim (not_eq_nil_append_cons ? ? ? ? H6)
            | elim H4;
              right;
-             apply (ex_intro ? ? (FFalse::a));
+             apply (ex_intro ? ? (FFalse::a1));
              simplify;
              elim H5;
-             apply (ex_intro ? ? a1);
+             apply (ex_intro ? ? a2);
              autobatch
            |3,4: autobatch
            | assumption
@@ -631,7 +631,7 @@ lemma sizel_0_no_axiom_is_tautology:
              elim (not_eq_nil_append_cons ? ? ? ? H5)
            | right;
              elim H4;
-             apply (ex_intro ? ? (FAtom n::a));
+             apply (ex_intro ? ? (FAtom n::a1));
              simplify;
              elim H;
              autobatch
@@ -644,11 +644,11 @@ lemma sizel_0_no_axiom_is_tautology:
         ]
      ]
   | intro;
-    elim t;
+     elim a;
      [ elim H;
         [ left;
           elim H4;
-          apply (ex_intro ? ? (FTrue::a));
+          apply (ex_intro ? ? (FTrue::a1));
           simplify;
           elim H5;
           autobatch
@@ -668,7 +668,7 @@ lemma sizel_0_no_axiom_is_tautology:
      | elim H;
         [ left;
           elim H4;
-          apply (ex_intro ? ? (FAtom n::a));
+          apply (ex_intro ? ? (FAtom n::a1));
           simplify;
           elim H5;
           autobatch
@@ -747,21 +747,21 @@ lemma completeness_base:
  elim S 1; clear S;
  simplify in ⊢ (?→%→?);
  intros;
- elim (look_for_axiom t t1);
+ elim (look_for_axiom a b);
   [ decompose;
     rewrite > H2; clear H2;
     rewrite > H4; clear H4;
-    apply (ExchangeL ? a1 a2 (FAtom a));
-    apply (ExchangeR ? a3 a4 (FAtom a));
+    apply (ExchangeL ? a2 a3 (FAtom a1));
+    apply (ExchangeR ? a4 a5 (FAtom a1));
     apply Axiom 
-  | elim (sizel_0_no_axiom_is_tautology t t1 H H1 H2);
+  | elim (sizel_0_no_axiom_is_tautology a b H H1 H2);
      [ decompose;
        rewrite > H3;
-       apply (ExchangeL ? a a1 FFalse);
+       apply (ExchangeL ? a1 a2 FFalse);
        apply FalseL
      | decompose;
        rewrite > H3;
-       apply (ExchangeR ? a a1 FTrue);
+       apply (ExchangeR ? a1 a2 FTrue);
        apply TrueR
      ]
   ]