proposition: Lemma trans_incl {Σ''} (incl' : Σ' ⊑ Σ'') : Σ ⊑ Σ''.
proof: Proof. destruct incl as [? ->], incl' as [? ->]. exists (pr0 ++ pr1). now rewrite app_assoc. Defined.
imports: Program.Basics Program.Tactics Equations.Equations Coq.Vectors.VectorDef List Equations(Fin)