Skip to content

Instantly share code, notes, and snippets.

@DmxLarchey

DmxLarchey/gist:d02dc73db8aa2771345724b51a968920

Created February 2, 2024 15:43
Show Gist options
  • Save DmxLarchey/d02dc73db8aa2771345724b51a968920 to your computer and use it in GitHub Desktop.
Save DmxLarchey/d02dc73db8aa2771345724b51a968920 to your computer and use it in GitHub Desktop.
Download ZIP
Acc clos trans
Raw
gistfile1.txt
Require Import Relations.
Section Acc_clos_trans.
Variables (X : Type) (R : X -> X -> Prop).
Hint Constructors clos_trans : core.
Hint Resolve Acc_inv : core.
Lemma Acc_clos_trans x : Acc R x -> Acc (clos_trans _ R) x.
Proof.
induction 1.
constructor.
induction 1; eauto.
Qed.
End Acc_clos_trans.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment