proposition: Lemma example_6_func (P Q R : Type) : (P → (Q → R)) → ((P → Q) → (P → R)).
proof: Proof. intro f. intro g. intro p. apply f. exact p. apply g. exact p. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.World.Addition