main part of lfpxs_cpxs ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / lfpxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma
index 7e1b3291553ecfa0b71d127650980a3967f70f5f..bfee0b2865d26f5de671c41117ee0dde64de2106 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma
@@ -51,4 +51,8 @@ lemma lfpxs_inv_atom1: ∀h,G,L2.T. ⦃G, ⋆⦄ ⊢ ⬈*[h, T] L2 → L2 = ⋆.
 (* Basic_2A1: was just: lpxs_inv_atom2 *)
 lemma lfpxs_inv_atom2: ∀h,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] ⋆ → L1 = ⋆.
 /2 width=2 by TC_lpx_sn_inv_atom2/ qed-.
-*)
\ No newline at end of file
+*)
+
+(* Basic_2A1: removed theorems 1:
+              lpxs_pair
+*)