Fixpoint neg_norm_aux (p: form) (b: bool): form :=
    match b with
    | true =>
        (* Cases with a negation symbol in front. *)
        match p with
        | FVar sym => <{ ~sym }>
        | <{ true }> => <{ false }>
        | <{ false }> => <{ true }>
        | <{ p /\ q }> => FOr (neg_norm_aux p true) (neg_norm_aux q true)
        | <{ p \/ q }> => FAnd (neg_norm_aux p true) (neg_norm_aux q true)
        | <{ p -> q }> => FAnd (neg_norm_aux p false) (neg_norm_aux q true)
        | <{ ~p }> => neg_norm_aux p false
        end
    | false =>
        (* Cases without a negation symbol in front. *)
        match p with
        | FVar sym => <{ sym }>
        | <{ true }> => <{ true }>
        | <{ false }> => <{ false }>
        | <{ p /\ q }> => FAnd (neg_norm_aux p false) (neg_norm_aux q false)
        | <{ p \/ q }> => FOr (neg_norm_aux p false) (neg_norm_aux q false)
        | <{ p -> q }> => FImp (neg_norm_aux p false) (neg_norm_aux q false)
        | <{ ~p }> => neg_norm_aux p true
        end
    end.

Definition neg_norm (p: form): form := neg_norm_aux p false.

Inductive in_neg_norm: form -> Prop :=
| in_neg_norm_var (sym: string): in_neg_norm <{ sym }>
| in_neg_norm_var_neg (sym: string): in_neg_norm <{ ~sym }>
| in_neg_norm_true: in_neg_norm <{ true }>
| in_neg_norm_false: in_neg_norm <{ false }>
| in_neg_norm_and (p q: form): in_neg_norm p /\ in_neg_norm q -> in_neg_norm <{ p /\ q }>
| in_neg_norm_or (p q: form): in_neg_norm p /\ in_neg_norm q -> in_neg_norm <{ p \/ q }>
| in_neg_norm_imp (p q: form): in_neg_norm p /\ in_neg_norm q -> in_neg_norm <{ p -> q }>.

Theorem neg_norm_in_neg_norm (p: form): in_neg_norm (neg_norm p).
Proof.
    induction p.
    - constructor.
    - constructor.
    - constructor.
    - constructor. split; assumption.
    - constructor. split; assumption.
    - constructor. split; assumption.
   (* Case <{ ~p }> *)
    - admit.
Admitted.