X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fmodels%2Fveq.ma;h=4d3d16c1e2ca2be618b74b76c9cca1991c93d48a;hp=a351e2003e38fa3a2bb3c2c5d6b68b76c63436b7;hb=cc600ed1e115d5566947288d532a1e89d989227f;hpb=ea918ec7701db4458c5ca25885e80abc6fed1be7

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma
index a351e2003..4d3d16c1e 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma
@@ -1,3 +1,4 @@
+
 (**************************************************************************)
 (*       ___                                                              *)
 (*      ||M||                                                             *)
@@ -87,7 +88,7 @@ lemma ti_comp (M): is_model M →
 [ /4 width=5 by seq_trans, seq_sym, ms/
 | /4 width=5 by seq_sym, ml, mq/
 | /4 width=3 by seq_trans, seq_sym, mg/
-| /5 width=5 by vpush_comp, seq_sym, md, mq/
+| /6 width=5 by vpush_comp, seq_sym, md, mc, mq/
 | /5 width=1 by vpush_comp, mi, mr/
 | /4 width=5 by seq_sym, ma, mp, mq/
 | /4 width=5 by seq_sym, me, mq/