(**************************************************************************)
include "basic_2/dynamic/snv_aaa.ma".
(**************************************************************************)
include "basic_2/dynamic/snv_aaa.ma".
include "basic_2/dynamic/lsubsv_lstas.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
include "basic_2/dynamic/lsubsv_lstas.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2
lapply (da_inv_bind … Hl1) -Hl1 #Hl1
elim (lstas_inv_bind1 … HT1U) -HT1U #U #HT2U #H destruct
elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2
lapply (da_inv_bind … Hl1) -Hl1 #Hl1
elim (lstas_inv_bind1 … HT1U) -HT1U #U #HT2U #H destruct
lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3
lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
lapply (IH2 … HW2l … HW23 … HL12) /2 width=1 by fqup_fpbg/ -HW2 -HW2l #HW3l
lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3
lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
lapply (IH2 … HW2l … HW23 … HL12) /2 width=1 by fqup_fpbg/ -HW2 -HW2l #HW3l
/4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/
| -U3
@(lsubsv_beta … (l-1)) /3 width=7 by fqup_fpbg/
/4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/
| -U3
@(lsubsv_beta … (l-1)) /3 width=7 by fqup_fpbg/
- @hsnv_cast [1,2: // ] #l0 #Hl0
- lapply (cpes_le_aux … IH4 IH3 IH2 IH1 … HW3l … HV2l … l0 … H32) -IH4 -IH3 -IH2 -IH1 -HW3l -HV2l -H32
+ @shnv_cast [1,2: // ] #l0 #Hl0
+ lapply (scpes_le_aux … IH4 IH3 IH2 IH1 … HW3l … HV2l … l0 … H32) -IH4 -IH3 -IH2 -IH1 -HW3l -HV2l -H32
/3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/
| -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbg, lpr_pair/
]
/3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/
| -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbg, lpr_pair/
]