the newly generated web pages ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / frees.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma
index e5e5b098c37b96ce921c36d9444932dc3adbaa0b..d9e58322597da7e80d59e3ac6bb0ad49e8f0f898 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma
@@ -184,3 +184,15 @@ lemma frees_gref_gen: ∀L,p,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃§p⦄ ≡ f.
 #L elim L -L
 /4 width=3 by frees_eq_repl_back, frees_gref, frees_atom, eq_push_inv_isid/
 qed.
+
+(* Basic_2A1: removed theorems 27:
+              frees_eq frees_be frees_inv
+              frees_inv_sort frees_inv_gref frees_inv_lref frees_inv_lref_free
+              frees_inv_lref_skip frees_inv_lref_ge frees_inv_lref_lt
+              frees_inv_bind frees_inv_flat frees_inv_bind_O
+              frees_lref_eq frees_lref_be frees_weak
+              frees_bind_sn frees_bind_dx frees_flat_sn frees_flat_dx
+              lreq_frees_trans frees_lreq_conf
+              llor_atom llor_skip llor_total
+              llor_tail_frees llor_tail_cofrees
+*)