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