proposition: Lemma FIB_HS2 x y z : sub x y -> sub y z -> sub x z.
proof: Proof. destruct x as [ [s HS]|], y as [ [t HT]|], z as [ [u HU]|]; cbn; auto. intros [H1[s' HS'] ] [H2[t' HT'] ]. subst. split. - rewrite app_assoc. intros H % app_eq_nil'. apply app_eq_nil in H as [-> ->]. now apply H1. - exists (t'++s'). apply app_assoc. 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