X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Frc_sat.ma;h=3eb04315f4f471a07e314b14086a574dc1cc0067;hb=53f874fba5b9c39a788085515a4fefe5d29281da;hp=aacaaed2b3e487c50119af2092b5906482baaa3c;hpb=eac90ccb93a94f03df9ba5ad853cbd5d8c60b4f2;p=helm.git

diff --git a/matita/matita/lib/lambda/rc_sat.ma b/matita/matita/lib/lambda/rc_sat.ma
index aacaaed2b..3eb04315f 100644
--- a/matita/matita/lib/lambda/rc_sat.ma
+++ b/matita/matita/lib/lambda/rc_sat.ma
@@ -33,6 +33,7 @@ record RC : Type[0] ≝ {
    sat3: SAT3 mem;  (* we add the clusure by rev dapp *)
    sat4: SAT4 mem   (* we add the clusure by dummies *) 
 }.
+
 (* HIDDEN BUG:
  * if SAT0 and SAT1 are expanded,
  * the projections sat0 and sat1 are not generated
@@ -119,7 +120,7 @@ qed.
 definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C.
 
 lemma dep_cr1: ∀B,C. CR1 (dep_mem B C).
-#B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) /2 by SAT0_sort/ /3/ (**) (* adiacent auto *)
+#B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) -Hdep /3/ @SAT0_sort //
 qed.
 
 lemma dep_sat0: ∀B,C. SAT0 (dep_mem B C).
@@ -134,7 +135,7 @@ lemma dep_sat2: ∀B,C. SAT2 (dep_mem B C).
 qed.
 
 lemma dep_sat3: ∀B,C. SAT3 (dep_mem B C).
-#B #C #N #l1 #l2 #HN #M #HM <appl_append >associative_append /3/
+#B #C #M #N #l #H #L #HL <appl_append @sat3 /2/
 qed.
 
 lemma dep_sat4: ∀B,C. SAT4 (dep_mem B C).