(* Advanced eliminators for native type assignment **************************)
lemma ntas_ind_bi_nta (h) (a) (G) (L) (Q:relation3 …):
- (â\88\80T1,T2. â¦\83G,Lâ¦\84 â\8a¢ T1 ![h,a] â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T2 ![h,a] â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 ⬌*[h] T2 →
+ (â\88\80T1,T2. â\9dªG,Lâ\9d« â\8a¢ T1 ![h,a] â\86\92 â\9dªG,Lâ\9d« â\8a¢ T2 ![h,a] â\86\92 â\9dªG,Lâ\9d« ⊢ T1 ⬌*[h] T2 →
Q 0 T1 T2
) →
- (â\88\80T1,T2. â¦\83G,Lâ¦\84 ⊢ T1 :[h,a] T2 → Q 1 T1 T2
+ (â\88\80T1,T2. â\9dªG,Lâ\9d« ⊢ T1 :[h,a] T2 → Q 1 T1 T2
) →
- (â\88\80n1,n2,T1,T2,T0. â¦\83G,Lâ¦\84 â\8a¢ T1 :*[h,a,n1] T0 â\86\92 â¦\83G,Lâ¦\84 ⊢ T0 :*[h,a,n2] T2 →
+ (â\88\80n1,n2,T1,T2,T0. â\9dªG,Lâ\9d« â\8a¢ T1 :*[h,a,n1] T0 â\86\92 â\9dªG,Lâ\9d« ⊢ T0 :*[h,a,n2] T2 →
Q n1 T1 T0 → Q n2 T0 T2 → Q (n1+n2) T1 T2
) →
- â\88\80n,T1,T2. â¦\83G,Lâ¦\84 ⊢ T1 :*[h,a,n] T2 → Q n T1 T2.
+ â\88\80n,T1,T2. â\9dªG,Lâ\9d« ⊢ T1 :*[h,a,n] T2 → Q n T1 T2.
#h #a #G #L #Q #IH1 #IH2 #IH3 #n
@(nat_elim1 n) -n * [| * ]
[ #_ #T1 #T2 #H
lemma nta_ind_cnv (h) (a) (Q:relation4 …):
(∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
(∀G,K,V,W,U.
- â¦\83G,Kâ¦\84 â\8a¢ V :[h,a] W â\86\92 â¬\86*[1] W ≘ U →
+ â\9dªG,Kâ\9d« â\8a¢ V :[h,a] W â\86\92 â\87§*[1] W ≘ U →
Q G K V W → Q G (K.ⓓV) (#0) U
) →
- (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h,a] â\86\92 â¬\86*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+ (â\88\80G,K,W,U. â\9dªG,Kâ\9d« â\8a¢ W ![h,a] â\86\92 â\87§*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
(∀I,G,K,W,U,i.
- â¦\83G,Kâ¦\84 â\8a¢ #i :[h,a] W â\86\92 â¬\86*[1] W ≘ U →
- Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
+ â\9dªG,Kâ\9d« â\8a¢ #i :[h,a] W â\86\92 â\87§*[1] W ≘ U →
+ Q G K (#i) W → Q G (K.ⓘ[I]) (#↑i) U
) →
(∀p,I,G,K,V,T,U.
- â¦\83G,Kâ¦\84 â\8a¢ V ![h,a] â\86\92 â¦\83G,K.â\93\91{I}Vâ¦\84 ⊢ T :[h,a] U →
- Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U)
+ â\9dªG,Kâ\9d« â\8a¢ V ![h,a] â\86\92 â\9dªG,K.â\93\91[I]Vâ\9d« ⊢ T :[h,a] U →
+ Q G (K.ⓑ[I]V) T U → Q G K (ⓑ[p,I]V.T) (ⓑ[p,I]V.U)
) →
(∀p,G,L,V,W,T,U0,U. (**) (* one IH is missing *)
- ad a 0 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ V :[h,a] W â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,0] â\93\9b{p}W.U0 â\86\92 â¦\83G,L.â\93\9bWâ¦\84 ⊢ U0 :[h,a] U →
- Q G L V W (* → Q G (L.ⓛW) U0 U *) → Q G L (ⓐV.T) (ⓐV.ⓛ{p}W.U)
+ ad a 0 â\86\92 â\9dªG,Lâ\9d« â\8a¢ V :[h,a] W â\86\92 â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,0] â\93\9b[p]W.U0 â\86\92 â\9dªG,L.â\93\9bWâ\9d« ⊢ U0 :[h,a] U →
+ Q G L V W (* → Q G (L.ⓛW) U0 U *) → Q G L (ⓐV.T) (ⓐV.ⓛ[p]W.U)
) →
(∀n,p,G,L,V,W,T,U,U0.
- ad a (â\86\91n) â\86\92 â¦\83G,Lâ¦\84 â\8a¢ V :[h,a] W â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T :[h,a] U â\86\92 â¦\83G,Lâ¦\84 â\8a¢ U :*[h,a,n] â\93\9b{p}W.U0 →
+ ad a (â\86\91n) â\86\92 â\9dªG,Lâ\9d« â\8a¢ V :[h,a] W â\86\92 â\9dªG,Lâ\9d« â\8a¢ T :[h,a] U â\86\92 â\9dªG,Lâ\9d« â\8a¢ U :*[h,a,n] â\93\9b[p]W.U0 →
Q G L V W → Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
) →
- (â\88\80G,L,T,U. â¦\83G,Lâ¦\84 ⊢ T :[h,a] U → Q G L T U → Q G L (ⓝU.T) U
+ (â\88\80G,L,T,U. â\9dªG,Lâ\9d« ⊢ T :[h,a] U → Q G L T U → Q G L (ⓝU.T) U
) →
(∀G,L,T,U1,U2.
- â¦\83G,Lâ¦\84 â\8a¢ T :[h,a] U1 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ U1 â¬\8c*[h] U2 â\86\92 â¦\83G,Lâ¦\84 ⊢ U2 ![h,a] →
+ â\9dªG,Lâ\9d« â\8a¢ T :[h,a] U1 â\86\92 â\9dªG,Lâ\9d« â\8a¢ U1 â¬\8c*[h] U2 â\86\92 â\9dªG,Lâ\9d« ⊢ U2 ![h,a] →
Q G L T U1 → Q G L T U2
) →
- â\88\80G,L,T,U. â¦\83G,Lâ¦\84 ⊢ T :[h,a] U → Q G L T U.
+ â\88\80G,L,T,U. â\9dªG,Lâ\9d« ⊢ T :[h,a] U → Q G L T U.
#h #a #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #H9 #G #L #T
@(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ]
[ #s #HG #HL #HT #X #H destruct -IH