Its for soundness theorem. I need to prove that the axioms (∀x)A -> A[t/x] its valid in constant domain semantics. I assume theres a world in a arbitrary model within (∀x)A -> A[t/x] its false and i search a contraddiction. (∀x)A -> A[t/x] its false when (∀x)A its true and A[t/x] its false. (∀x)A its true when A its true for each objects o in U (or D, the domain) that the valuaction function v assigns to the variable, but i dont understand how to explain that A[t/x] its false in logic sintax.