proposition: Theorem transfer_statement (s: Statement et): (∀ v, eval_stmt et (A:=A) v s) → (∀ v, eval_stmt et (A:=B) v s).
proof: Proof. Proof with intuition auto. intros ? v. assert (v = (λ _ i, ab (ba (v _ i)))) as P. destruct i. intros a a0. symmetry... rewrite P, transfer_statement_and_vars... Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.categories MathClasses.theory.ua_mapped_operations