(* Basic_1: was: sc3_arity_csubc *)
theorem acr_aaa_lsubc_lifts (RR) (RS) (RP):
gcp RR RS RP → gcr RR RS RP RP →
- â\88\80G,L1,T,A. â\9dªG,L1â\9d« ⊢ T ⁝ A → ∀b,f,L0. ⇩*[b,f] L0 ≘ L1 →
+ â\88\80G,L1,T,A. â\9d¨G,L1â\9d© ⊢ T ⁝ A → ∀b,f,L0. ⇩*[b,f] L0 ≘ L1 →
∀T0. ⇧*[f] T ≘ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
- â\9dªG,L2,T0â\9d« ϵ ⟦A⟧[RP].
+ â\9d¨G,L2,T0â\9d© ϵ ⟦A⟧[RP].
#RR #RS #RP #H1RP #H2RP #G #L1 #T @(fqup_wf_ind_eq (Ⓣ) … G L1 T) -G -L1 -T
#Z #Y #X #IH #G #L1 * [ * | * [ #p ] * ]
[ #s #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct
lapply (acr_gcr … H1RP H2RP A) #HA
lapply (drops_trans … HL01 … HLK1 ??) -HL01 [3: |*: // ] #H
- elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY
+ elim (drops_split_trans … H) -H [ |*: /2 width=6 by pr_after_nat_uni/ ] #Y #HLK0 #HY
lapply (drops_tls_at … Hf … HY) -Hf -HY #HY
elim (drops_inv_skip2 … HY) -HY #Z #K0 #HK01 #HZ #H destruct
elim (liftsb_inv_pair_sn … HZ) -HZ #V0 #HV10 #H destruct
(* Basic_1: was: sc3_arity *)
lemma acr_aaa (RR) (RS) (RP):
gcp RR RS RP → gcr RR RS RP RP →
- â\88\80G,L,T,A. â\9dªG,Lâ\9d« â\8a¢ T â\81\9d A â\86\92 â\9dªG,L,Tâ\9d« ϵ ⟦A⟧[RP].
+ â\88\80G,L,T,A. â\9d¨G,Lâ\9d© â\8a¢ T â\81\9d A â\86\92 â\9d¨G,L,Tâ\9d© ϵ ⟦A⟧[RP].
/3 width=9 by drops_refl, lifts_refl, acr_aaa_lsubc_lifts/ qed.
lemma gcr_aaa (RR) (RS) (RP):
gcp RR RS RP → gcr RR RS RP RP →
- â\88\80G,L,T,A. â\9dªG,Lâ\9d« ⊢ T ⁝ A → RP G L T.
+ â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A → RP G L T.
#RR #RS #RP #H1RP #H2RP #G #L #T #A #HT
lapply (acr_gcr … H1RP H2RP A) #HA
@(s1 … HA) /2 width=4 by acr_aaa/