- exclusion binder in local environments

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / i_static / tc_lfxs_tc_lfxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma
index 4fe37f452fea53af2ee126ed9f17db8a6c7dee1c..62173d926824eda2f830180fd500f7fab5a9b53b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma
@@ -19,5 +19,5 @@ include "basic_2/i_static/tc_lfxs.ma".
 (* Main properties **********************************************************)
 
 theorem tc_lfxs_trans: ∀R,T. Transitive … (tc_lfxs R T).
-#R #T #L1 #L #HL1 #L2 #HL2 @(trans_TC … HL1 HL2) (**) (* auto fails *) 
+#R #T #L1 #L #HL1 #L2 #HL2 @(trans_TC … HL1 HL2) (**) (* auto fails *)
 qed-.