elim b in H10;simplify in H10;destruct;exists [apply t2]
reflexivity]
|*:assumption]
- |simplify;apply SA_Arrow;autobatch width=4
+ |simplify;autobatch width=5 size=11
|simplify;apply (SA_All ? ? ? ? ? (H2 ? H6 ?? H8 H9))
[assumption
|apply H4
- [apply WFE_cons
- [assumption
- |lapply (H2 ? H6 ? H7);autobatch]
- |change in ⊢ (???%) with (flift f 1);apply injective_flift;assumption
+ [autobatch depth=4 width=4 size=8
+ |change in ⊢ (???%) with (flift f 1);autobatch;
|intro;cases n;simplify;intros;autobatch depth=4
- |change in ⊢ (???%) with (flift f 1);apply incl_cons;assumption]]]
+ |change in ⊢ (???%) with (flift f 1);autobatch]]]
qed.
inverter JS_indinv for JSubtype (%?%).
theorem narrowing:∀G,G1,U,P,M,N.
- G1 ⊢ P ⊴ U →
+ G1 ⊢ P ⊴ U →
(∀G2,S,T.
G2@G1 ⊢ S ⊴ lift U (length ? G2) O →
- G2@G1 ⊢ lift U (length ? G2) O ⊴ T \to
+ G2@G1 ⊢ lift U (length ? G2) O ⊴ T →
G2@G1 ⊢ S ⊴ T) →
G ⊢ M ⊴ N →
∀l.G=l@(mk_bound true U::G1) → l@(mk_bound true P::G1) ⊢ M ⊴ N.
|apply H6;reflexivity]]
qed.
-lemma JS_trans_prova: ∀T,G1.WFType G1 T →
-∀G,R,U,f.injective ?? f → length ? G1 ≤ length ? G → G ⊢ R ⊴ perm T f → G ⊢ perm T f ⊴ U → G ⊢ R ⊴ U.
-intros 3;elim H;clear H; try autobatch;
- [simplify in H5;simplify in H6;elim H5 using JS_indinv;destruct;autobatch
- |simplify in H4;inversion H4; intros; destruct; assumption
- |simplify in H7;elim H7 using JS_indinv;intros;destruct;
+lemma JS_trans_prova: ∀T,G,R,U,f.G ⊢ R ⊴ perm T f → G ⊢ perm T f ⊴ U → G ⊢ R ⊴ U.
+intro;elim T;
+ [simplify in H;simplify in H1;elim H using JS_indinv;destruct;autobatch
+ |simplify in H1;inversion H1; intros; destruct; assumption
+ |simplify in H2;elim H2 using JS_indinv;intros;destruct;
[autobatch
- |simplify in H8;inversion H8;intros;destruct;
- [apply SA_Top;autobatch;
- |apply SA_Arrow
- [apply (H2 ?????? H12 H);assumption
- |apply (H4 ?????? H10 H14);assumption]]]
- |simplify in H7;elim H7 using JS_indinv;intros;destruct;
+ |simplify in H3;inversion H3;intros;destruct;autobatch depth=4 size=7]
+ |simplify in H2;elim H2 using JS_indinv;intros;destruct;
[autobatch
- |simplify in H8;inversion H8;intros;destruct;
+ |simplify in H3;inversion H3;intros;destruct;
[apply SA_Top;autobatch
|apply SA_All
- [apply (H2 ?????? H12 H);assumption
- |apply H4
- [3:simplify;apply le_S_S;assumption
- |4:apply (narrowing (mk_bound true (perm t f)::G) G ???? H12 ? H10 [])
- [intros;rewrite > lift_perm2 in H16;rewrite > lift_perm2 in H17;
- rewrite > perm_compose in H16; rewrite > perm_compose in H17;
- apply H2
- [3:apply (trans_le ??? H6);rewrite > length_append;autobatch
- |4:apply H16
- |5:apply H17
- |2:apply injective_compose;autobatch]
+ [apply (H ???? H8 H4);assumption
+ |apply H1
+ [2:apply (narrowing (mk_bound true (perm t f)::G) G ???? H8 ? H6 [])
+ [intros;rewrite > lift_perm2 in H12;rewrite > lift_perm2 in H13;
+ rewrite > perm_compose in H12; rewrite > perm_compose in H13;
+ apply H
+ [2,3:autobatch]
|reflexivity]
- |5:assumption
- |2:change in ⊢ (???%) with (flift f 1);autobatch]]]]]
+ |3:assumption]]]]]
qed.
theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V.
intros 4;rewrite > (perm_id ? 0) in ⊢ (???% → ??%? → ?);
-intros;apply (JS_trans_prova ????????? H H1)
-[apply G
-|rewrite < perm_id in H;autobatch
-|simplify;intros;assumption
-|apply le_n]
+intros;autobatch;
qed.
theorem JS_narrow : ∀G1,G2,P,Q,T,U.
(G2 @ (mk_bound true P :: G1)) ⊢ T ⊴ U.
intros; apply (narrowing ? ? ? ? ? ? H1 ? H) [|autobatch]
intros;autobatch;
-qed.
+qed.
\ No newline at end of file