lemma coafter_isid_inv_dx: āf1,f2,f. f1 ~ā f2 ā” f ā šā¦f2ā¦ ā šā¦fā¦.
/4 width=4 by eq_id_isid, coafter_isid_dx, coafter_mono/ qed-.
-(* Properties with uniform relocations **************************************)
+(* Properties with test for 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/
+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.
-(*
-(* Properties on isuni ******************************************************)
+
+(*
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/
/3 width=5 by coafter_next/
]
qed.
+*)
-(* Properties on uni ********************************************************)
+(* 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/
(* 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.
+ āā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 ]
qed-.
lemma coafter_fwd_at: āi,i2,i1,f1,f2. @ā¦i1, f1ā¦ ā” i2 ā @ā¦i2, f2ā¦ ā” i ā
- āf. f2 ~ā f1 ā” f ā @ā¦i1, fā¦ ā” 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
qed-.
lemma coafter_fwd_at2: āf,i1,i. @ā¦i1, fā¦ ā” i ā āf1,i2. @ā¦i1, f1ā¦ ā” i2 ā
- āf2. f2 ~ā f1 ā” f ā @ā¦i2, f2ā¦ ā” i.
+ ā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.
+ ā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
(* Properties with at *******************************************************)
lemma coafter_uni_dx: āi2,i1,f2. @ā¦i1, f2ā¦ ā” i2 ā
- āf. f2 ~ā šā“i1āµ ā” f ā šā“i2āµ ~ā ā«±*[i2] f2 ā” f.
+ ā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
qed.
lemma coafter_uni_sn: āi2,i1,f2. @ā¦i1, f2ā¦ ā” i2 ā
- āf. šā“i2āµ ~ā ā«±*[i2] f2 ā” f ā f2 ~ā šā“i1āµ ā” f.
+ ā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
qed-.
lemma coafter_uni_succ_dx: āi2,i1,f2. @ā¦i1, f2ā¦ ā” i2 ā
- āf. f2 ~ā šā“ā«Æi1āµ ā” f ā šā“ā«Æi2āµ ~ā ā«±*[ā«Æi2] f2 ā” f.
+ ā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
qed.
lemma coafter_uni_succ_sn: āi2,i1,f2. @ā¦i1, f2ā¦ ā” i2 ā
- āf. šā“ā«Æi2āµ ~ā ā«±*[ā«Æi2] f2 ā” f ā f2 ~ā šā“ā«Æi1āµ ā” f.
+ ā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