λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / cnv_fqus.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma
index 50e4edbee00f04ccd9d58d09a0bdfcbea546ead6..7498e33c199b8fce1af06915ac4d869a780f65e7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma
@@ -38,7 +38,7 @@ lemma cnv_fqu_conf (h) (a):
   [ elim (cnv_inv_appl … H) -H //
   | elim (cnv_inv_cast … H) -H //
   ]
-| #I1 #G1 #L1 #T1 #U1 #HTU1 #HU 
+| #I1 #G1 #L1 #T1 #U1 #HTU1 #HU
   /4 width=7 by cnv_inv_lifts, drops_refl, drops_drop/
 ]
 qed-.