X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees_fqup.ma;h=9bbc83a891bcd3c61874299e509d5bc0fb126d16;hb=86d7622f88247d83b2c366a722d2994a4af91929;hp=8c89346f0d771b191962572fea9d59d5c29122bf;hpb=b7de6afb9d3260ffea86ddf824e497419e1b56fb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
index 8c89346f0..9bbc83a89 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
@@ -67,7 +67,7 @@ elim (pn_split f2) * #g2 #H destruct
   lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1
   lapply (sor_eq_repl_back1 … Hz … H02) -g0 #Hz
   lapply (sor_eq_repl_back2 … Hz … H1) -z1 #Hz
-  lapply (sor_sym … Hz) -Hz #Hz
+  lapply (sor_comm … Hz) -Hz #Hz
   lapply (sor_mono … f Hz ?) // -Hz #H
   lapply (sor_inv_sle_sn … Hf) -Hf #Hf
   lapply (frees_eq_repl_back … Hf0 (⫯f) ?) /2 width=5 by eq_next/ -z #Hf0
@@ -96,6 +96,6 @@ elim (pn_split f0) * #g0 #H destruct
   lapply (sor_eq_repl_back1 … Hg2 … H0) -z0 #Hg2
   lapply (sor_eq_repl_back2 … Hg2 … H1) -z1 #Hg2
   @(ex3_2_intro … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
-  /2 width=3 by sor_trans2_idem/
+  /2 width=3 by sor_comm_23_idem/
 ]
 qed-.