proposition: Lemma ienc_inj s t : ienc s =/= i_dum -> ienc s == ienc t -> s = t.
proof: Proof. Proof using HF3 HF2 HF1 HE2. revert t. induction s; intros [|]; cbn; trivial. - intros _ H. apply HE2 in H. now apply HF1 in H. - intros _ H. now apply HF1 in H. - intros H [H' ->] % HF2; trivial. f_equal. apply IHs; trivial. apply HF3 in H. trivial. Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation