[ create a new paste ] login | about

Link: http://codepad.org/vr1wO4O3    [ raw code | output | fork ]

OCaml, pasted on Oct 15:
Variable T : Set.
Variable A : T -> Prop.
Variable B : Prop.

Variable T_nonempty : T.

Definition lhs
  := (exists x, A x) -> B.

Definition rhs
  := forall x, (A x -> B).

Theorem dir_b
  : rhs -> lhs.
Proof.
  unfold lhs. unfold rhs. intros HA HE.
  inversion HE. apply HA with x. apply H.
Qed.

Theorem dir_a
  : lhs -> rhs.
Proof.
  unfold lhs. unfold rhs. intros HE x HA.
  apply HE. exists x. apply HA.
Qed.

Theorem both
  : lhs <-> rhs.
Proof.
  unfold iff. split. apply dir_a. apply dir_b.
Qed.


Output:
1
2
Line 1, characters 11-12:
Syntax error


Create a new paste based on this one


Comments: