X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpreamble.ma;h=958f1059a053b90a4f7f0fea0a9c39a8a3c72555;hb=1e8607eee93cec71e1d4d3bb93e321a460f59cec;hp=640615d596f2aa2aa2947a23884d7a3ec9b09916;hpb=5e8c551acfb4521d48256ae60042c07f9ee1be67;p=helm.git

diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma
index 640615d59..958f1059a 100644
--- a/matita/matita/contribs/lambda/preamble.ma
+++ b/matita/matita/contribs/lambda/preamble.ma
@@ -100,3 +100,14 @@ interpretation "map_cons" 'ho_cons a l = (map_cons ? a l).
 notation "hvbox(a ::: break l)"
   right associative with precedence 47
   for @{'ho_cons $a $l}.
+
+(* lstar *)
+
+(* Note: this cannot be in lib because of the missing xoa quantifier *)
+lemma lstar_inv_pos: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → 0 < |l| →
+                     ∃∃a,ll,b. a::ll = l & R a b1 b & lstar A B R ll b b2.
+#A #B #R #l #b1 #b2 #H @(lstar_ind_l ????????? H) -b1
+[ #H elim (lt_refl_false … H) 
+| #a #ll #b1 #b #Hb1 #Hb2 #_ #_ /2 width=6/ (**) (* auto fail if we do not remove the inductive premise *)
+]
+qed-.