proposition: Theorem F2 : Tautology (Node Impl (Node ANd (Node Impl (V (rnext zero)) (V (rnext (rnext zero)))) (Node Impl (V (rnext (rnext (rnext zero)))) (V (rnext (rnext (rnext (rnext zero))))))) (Node Impl (Node ANd (V (rnext zero)) (V (rnext (rnext (rnext zero))))) (Node ANd (V (rnext (rnext zero))) (V (rnext (rnext (rnext (rnext zero)))))))).
proof: Proof. apply (runC 0); exact (refl_equal true). Qed.
imports: Coq(ZArith)