Skip to content

Instantly share code, notes, and snippets.

@pirapira

pirapira/kanji.v

Created June 29, 2013 05:21
Show Gist options
  • Save pirapira/5889937 to your computer and use it in GitHub Desktop.
Save pirapira/5889937 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
kanji.v
Require Import ssreflect ssrbool eqtype ssrnat seq ssrfun fintype.
Ltac 破 := case.
Ltac 解 := elim.
Ltac 動 := move.
Ltac 割 := split.
Ltac 矣 := done.
Ltac 用 := apply.
Ltac 在 := exists.
Lemma andC {A B} : A /\ B -> B /\ A.
Proof.
破 => a b.
割; 矣.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment