(* Basic inversion lemmas ***************************************************)
-lemma csxv_inv_cons: â\88\80h,G,L,T,Ts. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T⨮Tsâ¦\84 →
- â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Tâ¦\84 â\88§ â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Tsâ¦\84.
+lemma csxv_inv_cons: â\88\80h,G,L,T,Ts. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªT⨮Tsâ\9d« →
+ â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d« â\88§ â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTsâ\9d«.
normalize // qed-.
(* Basic forward lemmas *****************************************************)
-lemma csx_fwd_applv: â\88\80h,G,L,T,Vs. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83â\92¶Vs.Tâ¦\84 →
- â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Vsâ¦\84 â\88§ â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Tâ¦\84.
+lemma csx_fwd_applv: â\88\80h,G,L,T,Vs. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªâ\92¶Vs.Tâ\9d« →
+ â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªVsâ\9d« â\88§ â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d«.
#h #G #L #T #Vs elim Vs -Vs /2 width=1 by conj/
#V #Vs #IHVs #HVs
lapply (csx_fwd_pair_sn … HVs) #HV