proposition: Lemma last_Forall A (x y : A) l P : last l x = y → Forall P l → P x → P y.
proof: Proof. generalize dependent x. destruct l using rev_ind; simpl; intros. now subst. rewrite last_rcons in H; subst. apply Forall_app in H0. destruct H0. now inversion H0. Qed.
imports: Coq.Lists.List Category.Lib.Tactics