initial properies of the "same top term constructor" predicate

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / grammar / thom.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma
index 15349202842bd26aa0da48e43af8a83a0b2d4827..5b90bd1d37bcbdb1a803253d520222a0046944e6 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma
@@ -76,8 +76,3 @@ lemma thom_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 →
                       ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] &
                                I = Appl & T2 = ⓐW2. U2.
 /2 width=4/ qed-.
-
-(* Basic_1: removed theorems 7:
-            iso_gen_sort iso_gen_lref iso_gen_head iso_refl iso_trans
-            iso_flats_lref_bind_false iso_flats_flat_bind_false
-*)