Skip to content

Instantly share code, notes, and snippets.

@psttf

psttf/comp_eq.v

Created April 24, 2018 11:54
Show Gist options
  • Save psttf/54a698861f4ba8f448b4277fd01eac78 to your computer and use it in GitHub Desktop.
Save psttf/54a698861f4ba8f448b4277fd01eac78 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
comp_eq.v
Definition compose {A: Type} (f g: A -> A) (x: A) := f (g x).
Lemma comp_eq: forall (A: Type) (f g: A -> A) (x: A), compose f g x = f (g x).
Proof.
intros.
unfold compose.
exact eq_refl.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment