Require Import ProofWeb. Variables p q: Prop. Lemma weak_pierce: ((((p -> q) -> p) -> p) -> q) -> q. Proof. imp_i h1. imp_e (((p -> q) -> p) -> p). assumption. imp_i h2. imp_e (p -> q). assumption. imp_i h3. imp_e (((p -> q) -> p) -> p). assumption. imp_i h4. assumption. Qed.