Inductive Bit: Set :=
  | Zer: Bit
  | One: Bit.

Inductive List (set1: Set): Set :=
  | Empt: List set1
  | Fill: set1 -> List set1 -> List set1.

Implicit Arguments Empt [[set1]].
Implicit Arguments Fill [[set1]].

Definition Nat: Set := List Bit.

Fixpoint Trim (nat1: Nat): Prop :=
  match nat1 with
  | Empt => True
  | Fill Zer Empt => False
  | Fill _ nat2 => Trim nat2
  end.

Theorem KQQP: Trim (Fill Zer Empt) = False.
Proof.
trivial.
Qed.

Theorem SLOF: forall nat1: Nat, Trim (Fill One nat1) = Trim nat1.
Proof.
trivial.
Qed.

Theorem GLBR: forall (bit1: Bit) (nat1: Nat), Trim (Fill bit1 nat1) -> Trim nat1.
Proof.
intros bit1 nat1 H1. destruct bit1.
  destruct nat1 as [ | bit2 nat2].
    rewrite KQQP in H1. contradiction.
    trivial.
  trivial.
Qed.

Definition trim (nat1: Nat): Nat :=
  match nat1 with
  | Fill Zer Empt => Empt
  | _ => nat1
  end.

Fixpoint pred (nat1: Nat): Nat :=
  match nat1 with
  | Empt => Empt
  | Fill Zer nat2 => Fill One (pred nat2)
  | Fill One nat2 => trim (Fill Zer nat2)
  end.

Theorem IEBL: forall nat1: Nat, pred (Fill Zer nat1) = Fill One (pred nat1).
Proof.
trivial.
Qed.

Theorem ZFAF: forall nat1: Nat, Trim nat1 -> Trim (pred nat1).
Proof.
intros nat1 H1. induction nat1 as [ | bit1 nat2 IHnat2].
  trivial.
  destruct bit1.
    apply GLBR in H1. specialize (IHnat2 H1). rewrite IEBL. rewrite SLOF. assumption.
    destruct nat2 as [ | bit2 nat3].
      trivial.
      trivial.
Qed.