Skip to content

Instantly share code, notes, and snippets.

@pi8027

pi8027/catIl.v

Last active June 21, 2020 20:39
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save pi8027/75e49ec71eda3fbe4ff7644270ae03d2 to your computer and use it in GitHub Desktop.
Save pi8027/75e49ec71eda3fbe4ff7644270ae03d2 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
catIl.v
Require Import all_ssreflect.
Section cat.
Variable (A : Type).
Lemma catIr : right_injective (@cat A).
Proof. by elim => //= ? ? IH ? ? [] /IH. Qed.
Lemma catIl : left_injective (@cat A).
Proof.
by move=> ? ? ? /(f_equal rev); rewrite !rev_cat => /catIr /(inv_inj revK).
(* elim/last_ind => [? ?|? ? IH ? ?]; rewrite ?cats0 // -!rcons_cat. *)
(* by move/(@rcons_injl A)/IH. *)
Qed.
End cat.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment