(* 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.
(* 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.