proposition: Lemma substitutive Γ t T Γ' u U : (Γ' @ (U :: Γ)) |-- t : T -> Γ |-- u : U -> Γ' @ Γ |-- subst (length Γ') t u : T.
proof: Proof. Proof with term. intros H. depind H; term. intros. assert (spec:=Nat.compare_spec i (length Γ')). depelim spec; try fold (length Γ') in H1; subst; try rewrite H1; try rewrite H2 ; simp subst. generalize (type_lift Γ0 u U [] H0 Γ'); simpl; intros. rewrite app_cons_snoc_app, app_nth1, app_nth2; try (simpl; lia). now rewrite Nat.sub_diag. term. rewrite app_nth1 by lia. rewrite <- (app_nth1 _ Γ0); term. rewrite app_nth2; term. change (U :: Γ0) with ((cons U nil) @ Γ0). rewrite app_nth2; term. simpl. rewrite (nth_extend_left unit _ Γ0 Γ'). replace (length Γ' + (i - length Γ' - 1)) with (pred i); term. apply axiom. autorewrite with list in H |- *. simpl in H. lia. intros. apply abstraction. now eapply (IHtypes _ _ _ (A :: Γ')). Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia