proposition: Lemma strict_incl_tran : forall A (l m n : list A), l [ m -> m [ n -> l [ n.
proof: Proof. unfold strict_incl. intuition. trans m; hyp. apply H2. trans n; hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)