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.