partial commit in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / fsle.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/fsle.ma b/matita/matita/contribs/lambdadelta/static_2/static/fsle.ma
index 659060756188b3c46265e5a6cda5acd723cfc0d6..5eb02293ee16ba9b14fad12344b590bbf531a75a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/fsle.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/fsle.ma
@@ -33,7 +33,7 @@ interpretation "free variables inclusion (term)"
 (* Basic properties *********************************************************)
 
 lemma fsle_sort: ∀L,s1,s2. ❪L,⋆s1❫ ⊆ ❪L,⋆s2❫.
-/3 width=8 by frees_sort, sle_refl, ex4_4_intro/ qed.
+/3 width=8 by frees_sort, pr_sle_refl, ex4_4_intro/ qed.
 
 lemma fsle_gref: ∀L,l1,l2. ❪L,§l1❫ ⊆ ❪L,§l2❫.
-/3 width=8 by frees_gref, sle_refl, ex4_4_intro/ qed.
+/3 width=8 by frees_gref, pr_sle_refl, ex4_4_intro/ qed.