proposition: Theorem eqConstrStateTransConstr : forall S : State, (forall a b c : rZ, eqConstrState S a (rZComp a) -> eqConstrState S b c) /\ (forall a b c : rZ, eqConstrState S a b -> eqConstrState S b c -> eqConstrState S a c).
proof: Proof. intros L; elim L; auto with stalmarck. split; intros a b c H'; inversion H'; auto with stalmarck. generalize H1; case a; intros; discriminate. intros p; case p. intros e f l H'; Elimc H'; intros H'0 H'1. split; [ intros a b c H'; inversion H'; generalize (H'0 a); generalize (fun b c : rZ => H'1 b a c); generalize (fun b c : rZ => H'1 b (rZComp a) c); intros Hc0 Hc1 Hc2; auto 4 with stalmarck | idtac ]. apply eqConstrStateContr; auto with stalmarck. apply Hc1; auto with stalmarck. rewrite <- (rZCompInv e); rewrite <- (rZCompInv a); apply eqConstrStateInv; auto with stalmarck. intros a b c H'; inversion H'; intros H'2; inversion H'2; generalize (H'0 f); generalize (fun a c : rZ => H'1 a b c); intros Hc0 Hc1; auto 4 with stalmarck. apply eqConstrStateTail. apply H'1 with (b := e); auto with stalmarck. apply eqConstrStateTail. apply H'1 with (b := f); auto with stalmarck. apply eqConstrStateTail; auto with stalmarck. apply H'0 with (a := e); auto with stalmarck. apply eqConstrStateTail; auto with stalmarck. apply H'1 with (b := rZComp e); auto with stalmarck. apply eqConstrStateTail; auto with stalmarck. apply H'0 with (a := e); auto with stalmarck. apply eqConstrStateTail; auto with stalmarck. apply H'1 with (b := rZComp f); auto with stalmarck. Qed.
imports: Coq(List)