include "basic_2/substitution/lpx_sn.ma".
(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
include "basic_2/substitution/lpx_sn.ma".
(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
#H #HV12 destruct @(ex3_2_intro … K2 V2) // -HV12
@conj // -HK12
#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (i+1)) -IH
#H #HV12 destruct @(ex3_2_intro … K2 V2) // -HV12
@conj // -HK12
#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (i+1)) -IH
#H #HV12 destruct @(ex3_2_intro … K1 V1) // -HV12
@conj // -HK12
#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (i+1)) -IH
#H #HV12 destruct @(ex3_2_intro … K1 V1) // -HV12
@conj // -HK12
#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (i+1)) -IH
qed-.
(* Basic properties *********************************************************)
lemma lpx_sn_alt_atom: ∀R. lpx_sn_alt R (⋆) (⋆).
#R @conj //
qed-.
(* Basic properties *********************************************************)
lemma lpx_sn_alt_atom: ∀R. lpx_sn_alt R (⋆) (⋆).
#R @conj //