proposition: Lemma supportTriplets : forall (f g : rNat -> bool) (l : list triplet), realizeTriplets f l -> equalBefore (rnext (maxVarTriplets l)) f g -> realizeTriplets g l.
proof: Proof. intros f g l; elim l; simpl in |- *; auto with stalmarck. intros a l0 H' H'0 H'1. red in |- *; simpl in |- *; auto with stalmarck. intros t H'2; Elimc H'2; intros H'2; [ rewrite <- H'2 | idtac ]; auto with stalmarck. apply trans_eq with (y := tEval f a); auto with stalmarck. apply sym_eq. apply equalBeforeTEval; auto with stalmarck. apply equalBeforeLt with (2 := H'1); auto with stalmarck. red in H'0; auto with datatypes stalmarck. lapply H'; clear H'; [ intros H'; lapply H'; clear H'; [ intros H' | idtac ] | idtac ]; auto with stalmarck. apply equalBeforeLt with (2 := H'1); auto with stalmarck. red in |- *; red in H'0; auto with datatypes stalmarck. Qed.
imports: Coq(Relation_Definitions)