proposition: Lemma subset_trans T (A1 A2 A3 : set T) : A1 \subset A2 -> A2 \subset A3 -> A1 \subset A3.
proof: Proof. now firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)