proposition: Lemma demo_applys : forall P : (nat -> nat) -> nat -> Prop, (forall f, P f (f 0)) -> P Dup 0.
proof: Proof. Proof using. intros. dup 4. apply (H Dup). apply H. refine (H _). applys H. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia