- we introduced the pointer_step rc in the perspective of proving

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / equivalence / cpcs_cpcs.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
index cf0b9030ca1f9ba4ec0fabe1a9fdd299a703bfac..ac9de93005c3be84d99e7045ad0b5281aedd88c2 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
@@ -164,7 +164,6 @@ elim (cpcs_inv_cprs … HT12) -HT12
 /3 width=5 by cprs_div, cprs_lsubs_trans/ (**) (* /3 width=5/ is a bit slow *)
 qed.
 
-
 (* Basic_1: was: pc3_lift *)
 lemma cpcs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
                  ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 →