proposition: Lemma sa_narrowing : forall {s} q, (forall {s'} (P : scope_le s s') (Γ : env O s') p (A : sa Γ p (lift_type_by P q)) s'' (Δ : env (S s') s'') a b (B : sa (env_app (cons (lift_type_by P q) Γ) Δ) a b), sa (env_app (cons p Γ) Δ) a b) /\ (forall {s'} (A : scope_le s s') (Γ : env O s') p (B : sa Γ p (lift_type_by A q)) r (C : sa Γ (lift_type_by A q) r), sa Γ p r).
proof: Proof. intros s q; induction q; match goal with | [ |- _ /\ ?Q ] => assert (PLOP:Q); [ intros s' A Γ p B; depind B; subst; intros r C; autorewrite with lift_type_by lift_var_by in *; try noconf H; try (constructor; auto; fail); try (constructor; eapply IHB; autorewrite with lift_type_by; auto; fail); try (depelim C; subst; constructor; destruct_pairs; try noconf H; eauto; fail); try (specialize (IHB _ _ _ IHq1 IHq2 A); destruct_pairs; try noconf H; constructor; eauto; fail); auto | split; [ intros s' P Γ p A; depind A; subst; intros s'' Δ a b B; destruct_pairs; remember (env_app (cons _ Γ) Δ) as PPP; depind B; try (subst; constructor; auto; autorewrite with core; auto; fail); clear B; constructor; specialize (IHB _ HeqPPP); subst *; try (noconf H; auto); match goal with | [ IHB : sa _ (lookup (env_app (cons ?a _) _) ?x) _ |- sa _ (lookup (env_app (cons ?b _) _) _) _ ] => destruct (var_dec_eq x (lift_var_by (env_scope_le Δ) FO)) as [Heq|Hneq] ; [ subst; autorewrite with lookup lift_type_by lift_var_by in *; try (noconf H; auto); autorewrite with lookup lift_type_by lift_var_by scope_le_app in *; try solve [auto; depelim IHB; autorewrite with lookup lift_type_by lift_var_by scope_le_app in *; auto; constructor; auto; fail]; try solve [(apply sa_var_trans in A || assert (A := sa_arr A1 A2) || assert (A := sa_all A1 A2)); match goal with | [ A : sa _ ?p _ |- _ ] => (apply @sa_weakening_app with (Δ:=cons p empty) in A; apply @sa_weakening_app with (Δ:=Δ) in A; autorewrite with lookup env_app lift_var_by lift_type_by in *; simpl in *; eapply PLOP; [exact A | exact IHB]) end; fail] | rewrite sa_toname with (p:=b) (q:=a); auto ] end | assumption ] ] end. - clear IHB1 IHB2. depelim C; [constructor|]; destruct_pairs. constructor; eauto. simpl in H. simpl in H0. apply (H1 _ A Γ _ C1 _ empty _ _) in B2; autorewrite with env_app in B2; eauto. Qed.
imports: Program Equations.Prop.DepElim Equations.Prop.Equations Coq.Logic.Eqdep_dec Coq.Classes.EquivDec Arith