proposition: Theorem eqConstrStateContrGen : forall (S : State) (a b c : rZ), eqConstrState S a (rZComp a) -> eqConstrState S b c.
proof: Proof. intros S a b c H'. elim (eqConstrStateTransConstr S); intros H'1 H'2; lapply (H'1 a b c); [ intros H'6; apply H'6 | idtac ]; auto with stalmarck. Qed.
imports: Coq(List)