proposition: Theorem realizeTripletIncl : forall (f : rNat -> bool) (L1 L2 : list triplet), realizeTriplets f L1 -> incl L2 L1 -> realizeTriplets f L2.
proof: Proof. intros f L1 L2 H'0 H'1; red in |- *; auto with stalmarck. Qed.