proposition: Theorem eqalters_I_bis : EqSt alter1 alter2.
proof: Proof. apply (buildeq SimplerInvariant). intros. case H. unfold T in |- *. intros. split. trivial. apply (makeinv (negb b)). apply (makeinv false). Qed.
imports: Bool