X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Fleq.ma;h=095e1ced3765ad8a590868ec495f1db205f84e1a;hb=e76eade57c0454a58b0d58e5484efe9af417847e;hp=32924d1c22dc73b7ec4f752cd9229dc03be27879;hpb=ab0d181f9a89f461a9c280f42a949a2dc2abe44c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma
index 32924d1c2..095e1ced3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma
@@ -44,6 +44,15 @@ lemma leq_sym: ∀L1,L2,d,e. L1 ≃[d, e] L2 → L2 ≃[d, e] L1.
 /2 width=1 by leq_atom, leq_zero, leq_pair, leq_succ/
 qed-.
 
+lemma leq_O_Y: ∀L1,L2. |L1| = |L2| → L1 ≃[0, ∞] L2.
+#L1 elim L1 -L1
+[ #X #H lapply (length_inv_zero_sn … H) -H //
+| #L1 #I1 #V1 #IHL1 #X #H elim (length_inv_pos_sn … H) -H
+  #L2 #I2 #V2 #HL12 #H destruct
+  @(leq_pair … (∞)) /2 width=1 by/ (**) (* explicit constructor *)
+]
+qed.
+
 (* Basic forward lemmas *****************************************************)
 
 lemma leq_fwd_length: ∀L1,L2,d,e. L1 ≃[d, e] L2 → |L1| = |L2|.