proposition: Theorem fInTCorrect : forall (LL : list triplet) (f : rZ -> _) (T : Trace), (forall n : rZ, incl (f n) LL) -> fInT f T = true -> TraceInList T LL.
proof: Proof. intros LL f T H'; elim T; simpl in |- *; auto with stalmarck. intros t; case t; auto with stalmarck. intros r r0 r1 r2; case (InDec _ tripletDec (Triplet r r0 r1 r2) (f r0)); auto with stalmarck. intros H'0 H'1; apply (H' r0); auto with stalmarck. intros; discriminate. intros t; case (fInT f t); auto with stalmarck. intros; discriminate. intros a b t; case (fInT f t); auto with stalmarck. intros; discriminate. Qed.
imports: Stalmarck(makeTriplet)