proposition: Lemma pres_in t : t ∈ Σ -> t ∈ Σ'.
proof: Proof. destruct incl. subst. clear. induction pr1. intros. exact H. intros H. specialize (IHpr1 H). constructor 2. apply IHpr1. Defined.
imports: Program.Basics Program.Tactics Equations.Equations Coq.Vectors.VectorDef List Equations(Fin)