proposition: Lemma lem_lam_4 : forall P : (nat -> nat -> nat) -> Prop, P (fun x y => match x with 0 => 0 | S z => z end + y) -> P (fun a b => match a with 0 => 0 | S z => z end + b).
proof: Proof. hammer. Qed.
imports: Hammer(Hammer) List