(* Basic properties *********************************************************)
-lemma fpbc_fpbg: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\89»â\8b\95[h, g] ⦃G2, L2, T2⦄ →
- â¦\83G1, L1, T1â¦\84 >â\8b\95[h, g] ⦃G2, L2, T2⦄.
+lemma fpbc_fpbg: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\89»â\89¡[h, g] ⦃G2, L2, T2⦄ →
+ â¦\83G1, L1, T1â¦\84 >â\89¡[h, g] ⦃G2, L2, T2⦄.
/2 width=1 by tri_inj/ qed.
lemma fpbg_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2.
- â¦\83G1, L1, T1â¦\84 >â\8b\95[h, g] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G, L, Tâ¦\84 â\89»â\8b\95[h, g] ⦃G2, L2, T2⦄ →
- â¦\83G1, L1, T1â¦\84 >â\8b\95[h, g] ⦃G2, L2, T2⦄.
+ â¦\83G1, L1, T1â¦\84 >â\89¡[h, g] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G, L, Tâ¦\84 â\89»â\89¡[h, g] ⦃G2, L2, T2⦄ →
+ â¦\83G1, L1, T1â¦\84 >â\89¡[h, g] ⦃G2, L2, T2⦄.
/2 width=5 by tri_step/ qed.
lemma fpbg_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2.
- â¦\83G1, L1, T1â¦\84 â\89»â\8b\95[h, g] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G, L, Tâ¦\84 >â\8b\95[h, g] ⦃G2, L2, T2⦄ →
- â¦\83G1, L1, T1â¦\84 >â\8b\95[h, g] ⦃G2, L2, T2⦄.
+ â¦\83G1, L1, T1â¦\84 â\89»â\89¡[h, g] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G, L, Tâ¦\84 >â\89¡[h, g] ⦃G2, L2, T2⦄ →
+ â¦\83G1, L1, T1â¦\84 >â\89¡[h, g] ⦃G2, L2, T2⦄.
/2 width=5 by tri_TC_strap/ qed.
(* Note: this is used in the closure proof *)
-lemma fqup_fpbg: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\90+ â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 >â\8b\95[h, g] ⦃G2, L2, T2⦄.
+lemma fqup_fpbg: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\90+ â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 >â\89¡[h, g] ⦃G2, L2, T2⦄.
/4 width=1 by fpbc_fpbg, fpbu_fpbc, fpbu_fqup/ qed.
(* Basic eliminators ********************************************************)
lemma fpbg_ind: ∀h,g,G1,L1,T1. ∀R:relation3 ….
- (â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89»â\8b\95[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- (â\88\80G,G2,L,L2,T,T2. â¦\83G1, L1, T1â¦\84 >â\8b\95[h, g] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G, L, Tâ¦\84 â\89»â\8b\95[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
- â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\8b\95[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2.
+ (â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89»â\89¡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ (â\88\80G,G2,L,L2,T,T2. â¦\83G1, L1, T1â¦\84 >â\89¡[h, g] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G, L, Tâ¦\84 â\89»â\89¡[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
+ â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\89¡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2.
#h #g #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
@(tri_TC_ind … IH1 IH2 G2 L2 T2 H)
qed-.
lemma fpbg_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 ….
- (â\88\80G1,L1,T1. â¦\83G1, L1, T1â¦\84 â\89»â\8b\95[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1) →
- (â\88\80G1,G,L1,L,T1,T. â¦\83G1, L1, T1â¦\84 â\89»â\8b\95[h, g] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G, L, Tâ¦\84 >â\8b\95[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
- â\88\80G1,L1,T1. â¦\83G1, L1, T1â¦\84 >â\8b\95[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1.
+ (â\88\80G1,L1,T1. â¦\83G1, L1, T1â¦\84 â\89»â\89¡[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1) →
+ (â\88\80G1,G,L1,L,T1,T. â¦\83G1, L1, T1â¦\84 â\89»â\89¡[h, g] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G, L, Tâ¦\84 >â\89¡[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
+ â\88\80G1,L1,T1. â¦\83G1, L1, T1â¦\84 >â\89¡[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1.
#h #g #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
@(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H)
qed-.