proposition: Lemma arr_eqI {s t: bool -> term} : (forall (a: bool), s a = t a) -> arr (s false) (s true) = arr (t false) (t true).
proof: Proof. move=> H. by rewrite ? H. Qed.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.StackMachines(SSM) Undecidability.StackMachines.Util(CSSM_facts) Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool