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