proposition: Theorem relate_correct : forall p q qpos rm, interp_pos_atom p rm -> match relate p q qpos with | ARimply => interp_atom q qpos rm | ARcontradict => not (interp_atom q qpos rm) | ARunknown => True end.
proof: Proof. intros p q qpos rm Hp. unfold relate. generalize (relate'_correct p q rm Hp). now destruct relate' ; case qpos. Qed.
imports: Reals List Bool Gappa_common