proposition: Lemma gamma_invol A : gamma (gamma A) = A.
proof: Proof. induction A as [ | (x,y) ]; cbn. - reflexivity. - simpl_list. now rewrite <- IHA at 2. Qed.
imports: List Lia Undecidability.CFG.CFP Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions