proposition: Lemma incl_trans : forall A dom₁ dom₂ dom3 (m₁ : t A dom₁) (m₂ : t A dom₂) (m3 : t A dom3), incl m₁ m₂ -> incl m₂ m3 -> incl m₁ m3.
proof: Proof. repeat intro. auto. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface