こう？

Require Import Omega.
Require Import Arith.
Open Scope Z_scope.

Definition tr(x:Z) := exists y:Z , x=3*y.
Definition s(x:Z) := exists y:Z,x=6*y.


Theorem t: forall x:Z,tr(x)->s(4*x).

intros.
unfold s.
destruct H.
exists (2*x0).
replace x with (3*x0).
omega.
Qed.

多分このスレには片山さんと俺しかいないぞｗ