-(* Properties with test for uniform relocations *****************************)
-
-lemma coafter_isuni_isid: ∀f2. 𝐈❪f2❫ → ∀f1. 𝐔❪f1❫ → f1 ~⊚ f2 ≘ f2.
-#f #Hf #g #H elim H -g
-/3 width=5 by coafter_isid_sn, coafter_eq_repl_back0, coafter_next, eq_push_inv_isid/
-qed.
-
-
-(*
-lemma coafter_isid_isuni: ∀f1,f2. 𝐈❪f2❫ → 𝐔❪f1❫ → f1 ~⊚ ↑f2 ≘ ↑f1.
-#f1 #f2 #Hf2 #H elim H -H
-/5 width=7 by coafter_isid_dx, coafter_eq_repl_back2, coafter_next, coafter_push, eq_push_inv_isid/
-qed.
-
-lemma coafter_uni_next2: ∀f2. 𝐔❪f2❫ → ∀f1,f. ↑f2 ~⊚ f1 ≘ f → f2 ~⊚ ↑f1 ≘ f.
-#f2 #H elim H -f2
-[ #f2 #Hf2 #f1 #f #Hf
- elim (coafter_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H0 destruct
- /4 width=7 by coafter_isid_inv_sn, coafter_isid_sn, coafter_eq_repl_back0, eq_next/
-| #f2 #_ #g2 #H2 #IH #f1 #f #Hf
- elim (coafter_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H0 destruct
- /3 width=5 by coafter_next/
-]
-qed.
-*)
-
-(* Properties with uniform relocations **************************************)
-
-lemma coafter_uni_sn: ∀i,f. 𝐔❨i❩ ~⊚ f ≘ ⫯*[i] f.
-#i elim i -i /2 width=5 by coafter_isid_sn, coafter_next/
-qed.
-
-(*
-lemma coafter_uni: ∀n1,n2. 𝐔❨n1❩ ~⊚ 𝐔❨n2❩ ≘ 𝐔❨n1+n2❩.
-@nat_elim2
-/4 width=5 by coafter_uni_next2, coafter_isid_sn, coafter_isid_dx, coafter_next/
-qed.
-
-(* Forward lemmas on at *****************************************************)
-
-lemma coafter_at_fwd: ∀i,i1,f. @❪i1, f❫ ≘ i → ∀f2,f1. f2 ~⊚ f1 ≘ f →
- ∃∃i2. @❪i1, f1❫ ≘ i2 & @❪i2, f2❫ ≘ i.
-#i elim i -i [2: #i #IH ] #i1 #f #Hf #f2 #f1 #Hf21
-[ elim (at_inv_xxn … Hf) -Hf [1,3:* |*: // ]
- [1: #g #j1 #Hg #H0 #H |2,4: #g #Hg #H ]
-| elim (at_inv_xxp … Hf) -Hf //
- #g #H1 #H
-]
-[2: elim (coafter_inv_xxn … Hf21 … H) -f *
- [ #g2 #g1 #Hg21 #H2 #H1 | #g2 #Hg21 #H2 ]
-|*: elim (coafter_inv_xxp … Hf21 … H) -f
- #g2 #g1 #Hg21 #H2 #H1
-]
-[4: -Hg21 |*: elim (IH … Hg … Hg21) -g -IH ]
-/3 width=9 by at_refl, at_push, at_next, ex2_intro/
-qed-.
-
-lemma coafter_fwd_at: ∀i,i2,i1,f1,f2. @❪i1, f1❫ ≘ i2 → @❪i2, f2❫ ≘ i →
- ∀f. f2 ~⊚ f1 ≘ f → @❪i1, f❫ ≘ i.
-#i elim i -i [2: #i #IH ] #i2 #i1 #f1 #f2 #Hf1 #Hf2 #f #Hf
-[ elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- #g2 [ #j2 ] #Hg2 [ #H22 ] #H20
- [ elim (at_inv_xxn … Hf1 … H22) -i2 *
- #g1 [ #j1 ] #Hg1 [ #H11 ] #H10
- [ elim (coafter_inv_ppx … Hf … H20 H10) -f1 -f2 /3 width=7 by at_push/
- | elim (coafter_inv_pnx … Hf … H20 H10) -f1 -f2 /3 width=6 by at_next/
- ]
- | elim (coafter_inv_nxx … Hf … H20) -f2 /3 width=7 by at_next/
- ]
-| elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H22 #H20
- elim (at_inv_xxp … Hf1 … H22) -i2 #g1 #H11 #H10
- elim (coafter_inv_ppx … Hf … H20 H10) -f1 -f2 /2 width=2 by at_refl/
-]
-qed-.
-
-lemma coafter_fwd_at2: ∀f,i1,i. @❪i1, f❫ ≘ i → ∀f1,i2. @❪i1, f1❫ ≘ i2 →
- ∀f2. f2 ~⊚ f1 ≘ f → @❪i2, f2❫ ≘ i.
-#f #i1 #i #Hf #f1 #i2 #Hf1 #f2 #H elim (coafter_at_fwd … Hf … H) -f
-#j1 #H #Hf2 <(at_mono … Hf1 … H) -i1 -i2 //
-qed-.
-
-lemma coafter_fwd_at1: ∀i,i2,i1,f,f2. @❪i1, f❫ ≘ i → @❪i2, f2❫ ≘ i →
- ∀f1. f2 ~⊚ f1 ≘ f → @❪i1, f1❫ ≘ i2.
-#i elim i -i [2: #i #IH ] #i2 #i1 #f #f2 #Hf #Hf2 #f1 #Hf1
-[ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
- #g [ #j1 ] #Hg [ #H01 ] #H00
- elim (at_inv_xxn … Hf2) -Hf2 [1,3,5,7: * |*: // ]
- #g2 [1,3: #j2 ] #Hg2 [1,2: #H22 ] #H20
- [ elim (coafter_inv_pxp … Hf1 … H20 H00) -f2 -f /3 width=7 by at_push/
- | elim (coafter_inv_pxn … Hf1 … H20 H00) -f2 -f /3 width=5 by at_next/
- | elim (coafter_inv_nxp … Hf1 … H20 H00)
- | /4 width=9 by coafter_inv_nxn, at_next/
- ]
-| elim (at_inv_xxp … Hf) -Hf // #g #H01 #H00
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H21 #H20
- elim (coafter_inv_pxp … Hf1 … H20 H00) -f2 -f /3 width=2 by at_refl/
-]
-qed-.
-
-(* Properties with at *******************************************************)
-
-lemma coafter_uni_dx: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
- ∀f. f2 ~⊚ 𝐔❨i1❩ ≘ f → 𝐔❨i2❩ ~⊚ ⫱*[i2] f2 ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
- lapply (coafter_isid_inv_dx … Hf ?) -Hf
- /3 width=3 by coafter_isid_sn, coafter_eq_repl_back0/
-| #i2 #IH #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- [ #g2 #j1 #Hg2 #H1 #H2 destruct
- elim (coafter_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
- /3 width=5 by coafter_next/
- | #g2 #Hg2 #H2 destruct
- elim (coafter_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- /3 width=5 by coafter_next/
- ]
-]
-qed.
-
-lemma coafter_uni_sn: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
- ∀f. 𝐔❨i2❩ ~⊚ ⫱*[i2] f2 ≘ f → f2 ~⊚ 𝐔❨i1❩ ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
- lapply (coafter_isid_inv_sn … Hf ?) -Hf
- /3 width=3 by coafter_isid_dx, coafter_eq_repl_back0/
-| #i2 #IH #i1 #f2 #Hf2 #f #Hf
- elim (coafter_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- [ #g2 #j1 #Hg2 #H1 #H2 destruct /3 width=7 by coafter_push/
- | #g2 #Hg2 #H2 destruct /3 width=5 by coafter_next/
- ]
-]
-qed-.
-
-lemma coafter_uni_succ_dx: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
- ∀f. f2 ~⊚ 𝐔❨↑i1❩ ≘ f → 𝐔❨↑i2❩ ~⊚ ⫱*[↑i2] f2 ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
- elim (coafter_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H
- lapply (coafter_isid_inv_dx … Hg ?) -Hg
- /4 width=5 by coafter_isid_sn, coafter_eq_repl_back0, coafter_next/
-| #i2 #IH #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- [ #g2 #j1 #Hg2 #H1 #H2 destruct
- elim (coafter_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
- /3 width=5 by coafter_next/
- | #g2 #Hg2 #H2 destruct
- elim (coafter_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- /3 width=5 by coafter_next/
- ]
-]
-qed.
-
-lemma coafter_uni_succ_sn: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
- ∀f. 𝐔❨↑i2❩ ~⊚ ⫱*[↑i2] f2 ≘ f → f2 ~⊚ 𝐔❨↑i1❩ ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
- elim (coafter_inv_nxx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
- lapply (coafter_isid_inv_sn … Hg ?) -Hg
- /4 width=7 by coafter_isid_dx, coafter_eq_repl_back0, coafter_push/
-| #i2 #IH #i1 #f2 #Hf2 #f #Hf
- elim (coafter_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- [ #g2 #j1 #Hg2 #H1 #H2 destruct <tls_xn in Hg; /3 width=7 by coafter_push/
- | #g2 #Hg2 #H2 destruct <tls_xn in Hg; /3 width=5 by coafter_next/
- ]
-]
-qed-.
-
-lemma coafter_uni_one_dx: ∀f2,f. ⫯f2 ~⊚ 𝐔❨↑O❩ ≘ f → 𝐔❨↑O❩ ~⊚ f2 ≘ f.
-#f2 #f #H @(coafter_uni_succ_dx … (⫯f2)) /2 width=3 by at_refl/
-qed.
-
-lemma coafter_uni_one_sn: ∀f1,f. 𝐔❨↑O❩ ~⊚ f1 ≘ f → ⫯f1 ~⊚ 𝐔❨↑O❩ ≘ f.
-/3 width=3 by coafter_uni_succ_sn, at_refl/ qed-.
-*)