proposition: Lemma stateAssignedProp2 : forall (S : State) (L : list triplet), stateAssignedOn S L -> forall a b : rZ, inTriplets a L -> inTriplets b L -> eqStateRz S a b \/ eqStateRz S a (rZComp b).
proof: Proof. intros S L H a b Ha Hb. case (inTripletsVarTriplet L a Ha); case (inTripletsVarTriplet L b Hb); intros H1 H2. apply (stateAssignedProp1 S L); auto with stalmarck. lapply (stateAssignedProp1 S L H a (rZComp b) H2); auto with stalmarck. rewrite (rZCompInv b); auto with stalmarck; intros Z; elim Z; simpl in |- *; auto with stalmarck. lapply (stateAssignedProp1 S L H (rZComp a) b H2); auto with stalmarck. intros Z; elim Z; intros Z1; auto with stalmarck; right; rewrite <- (rZCompInv a); auto with stalmarck. rewrite <- (rZCompInv a); rewrite <- (rZCompInv b). lapply (stateAssignedProp1 S L H (rZComp a) (rZComp b) H2); auto with stalmarck. intros Z; elim Z; simpl in |- *; auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux) Stalmarck(makeTriplet)