proposition: Theorem realizeTripletCons : forall (f : rNat -> bool) (t : triplet) (L : list triplet), tEval f t = true -> realizeTriplets f L -> realizeTriplets f (t :: L).
proof: Proof. intros f t L H' H'0; red in |- *; simpl in |- *. intros t0 H'1; elim H'1; intros H'2; auto with stalmarck; rewrite <- H'2; auto with stalmarck. Qed.