(* Basic inversion lemmas ***************************************************)
-lemma csnv_inv_cons: â\88\80L,T,Ts. L â\8a¢ â¬\87* T @ Ts â\86\92 L â\8a¢ â¬\87* T â\88§ L â\8a¢ â¬\87* Ts.
+lemma csnv_inv_cons: â\88\80L,T,Ts. L â\8a¢ â¬\8a* T @ Ts â\86\92 L â\8a¢ â¬\8a* T â\88§ L â\8a¢ â¬\8a* Ts.
normalize // qed-.