(* Basic inversion properties ***********************************************)
lemma cpr_inv_Delta1_body_sn (h) (G) (L) (s):
(* Basic inversion properties ***********************************************)
lemma cpr_inv_Delta1_body_sn (h) (G) (L) (s):
/5 width=3 by cpm_eps, cpm_appl, cpm_bind, cpm_delta, Delta_lifts/ qed.
/5 width=3 by cpm_eps, cpm_appl, cpm_bind, cpm_delta, Delta_lifts/ qed.
/4 width=3 by cpm_zeta, Delta_lifts, lifts_flat/ qed.
(* Main inversion properties ************************************************)
theorem cpr_inv_Omega1_sn (h) (G) (L) (s):
/4 width=3 by cpm_zeta, Delta_lifts, lifts_flat/ qed.
(* Main inversion properties ************************************************)
theorem cpr_inv_Omega1_sn (h) (G) (L) (s):
∨∨ Omega1 s = X | Omega2 s = X.
#h #G #L #s #X #H elim (cpm_inv_appl1 … H) -H *
[ #W2 #T2 #HW2 #HT2 #H destruct
∨∨ Omega1 s = X | Omega2 s = X.
#h #G #L #s #X #H elim (cpm_inv_appl1 … H) -H *
[ #W2 #T2 #HW2 #HT2 #H destruct