(* Main inversion lemmas ****************************************************)
theorem lveq_inv_bind: ∀K1,K2. K1 ≋ⓧ*[0,0] K2 →
(* Main inversion lemmas ****************************************************)
theorem lveq_inv_bind: ∀K1,K2. K1 ≋ⓧ*[0,0] K2 →