Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/練習問題: ★★★★, optional (true_upto_n__true_everywhere)

Created May 21, 2016 08:07
Show Gist options
  • Save yoshihiro503/7cc2a40211a9700b52ba001bac126c72 to your computer and use it in GitHub Desktop.
Save yoshihiro503/7cc2a40211a9700b52ba001bac126c72 to your computer and use it in GitHub Desktop.
Download ZIP
練習問題: ★★★★, optional (true_upto_n__true_everywhere)
Raw
練習問題: ★★★★, optional (true_upto_n__true_everywhere)
Fixpoint true_upto_n__true_everywhere
(* FILL IN HERE *)
Example true_upto_n_example :
(true_upto_n__true_everywhere 3 (fun n => even n))
= (even 3 -> even 2 -> even 1 -> forall m : nat, even m).
Proof. reflexivity. Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment