proposition: Lemma unenc_correct2 t n : nat_unenc t = Some n -> nat_enc n = t.
proof: Proof. Proof with try solve [Coq.Init.Tactics.easy]. revert n. eapply (size_induction (f := size) (p := (fun t => forall n, nat_unenc t = Some n -> nat_enc n = t))). clear t. intros t IHt n H. destruct t as [ | | t]. easy. easy. destruct t as [ | | t]. easy. easy. destruct t. 3:easy. - destruct n0. easy. destruct n0. 2:easy. inv H. easy. - destruct t1. 2-3:easy. destruct n0. 2:easy. simpl in H. destruct (nat_unenc t2) eqn:A. + apply IHt in A;simpl;try lia. destruct n. inv H. simpl. congruence. + congruence. Qed.
imports: Undecidability.Shared.Libs.PSL.Numbers Nat Undecidability.L(Datatypes.LBool Functions.EqBool Datatypes.LProd)