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