DeMorgan.fm

// Proof that !(P ∨ Q) == !P ∧ !Q
DeMorgan.Or.forward
    : <A: Type> ->
      <B: Type> ->
      Not(Or(A, B)) ->
      And(Not(A), Not(B))
    <A, B> (not_or)
    Pair.new<_, _>(
        (a) not_or(Either.left<_, _>(a)),
        (b) not_or(Either.right<_, _>(b))
    )

// Proof that !P ∧ !Q => !(P ∨ Q)
DeMorgan.Or.reverse
    : <A: Type> ->
      <B: Type> ->
      And(Not(A), Not(B)) ->
      Not(Or(A, B))
    <A, B> (and_not)
    ((or)
        case or:
        | (a)
          case and_not:
          | (not_a, not_b) not_a(a);;
        | (b)
          case and_not:
          | (not_a, not_b) not_b(b);;
    )

// Proof that !(P ∧ Q) => !P ∨ !Q
// Unconstructable as requires double negation
DeMorgan.And.forward
    : <A: Type> ->
      <B: Type> ->
      Classical.double_negation ->
      Not(And(A, B)) ->
      Or(Not(A), Not(B))
    <A, B> (dn, n_and)

    def non_to_nna = ((non)
        def and_nn = DeMorgan.Or.forward<Not(A), Not(B)>(non)
        def and = (
            case and_nn:
            | (nn_a, nn_b) Pair.new<A, B>(dn<_>(nn_a), dn<_>(nn_b));
        ) :: And(A, B)
        Not.p_to_nnp<And(A, B)>(and)
    ) :: Not(Or(Not(A), Not(B))) -> Not(Not(And(A, B)))

    def nnn_and = Not.p_to_nnp<_>(n_and)
    def nn_or_n = Contrapositive.type<_, _>(non_to_nna, nnn_and)

    dn<_>(nn_or_n)

// Proof that !P ∨ !Q => !(P ∧ Q)
DeMorgan.And.reverse
    : <A: Type> ->
      <B: Type> ->
      Or(Not(A), Not(B)) ->
      Not(And(A, B))
    <A, B> (or_not)
    ((and)
        case and:
        | (a, b)
          case or_not:
          | (not_a) not_a(a);
          | (not_b) not_b(b);;
    )