proposition: Theorem forall_bound_equiv : (forall n, A n -> P n) <-> (forall n, A n -> Q n).
proof: Proof. Proof using HPQ. split; intros H n Hn; generalize (H _ Hn); apply HPQ; auto. Qed.
imports: Arith List Wellfounded Extraction