proposition: Theorem dont_touch_forall3 : forall (P Q: nat -> [univ]), (forall n, P n <=> (forall m, Q (m+n))) -> (forall m, Q (m+1)) -> P 1.
proof: Proof. intros ? ? Hif Hq . trw_rev_h Hif Hq. trivial. Qed.
imports: universe Coq.Setoids.Setoid