proposition: Lemma H : forall z1 z2 : St, EqSt1 z1 z2 -> T EqSt1 z1 z2.
proof: Proof. intros z1 z2 x. red in |- *. case x. intros z3 z4 H0 H1. split. assumption. case H1. intro H2. case H2. apply eqalters_body. intros. assumption. Qed.
imports: Bool