Jan Ruzicka ruza-net
kyoDralliam
/ acc_idc.v
Created
March 18, 2022 12:44
Accessibility and extraction of infinite decending chains
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| From Equations Require Import Equations. | |
| From Coq Require Import ssreflect. | |
| Section Defs. | |
| Context {A : Type} (R : A -> A -> Prop). | |
| Definition entire := forall x, exists y, R y x. | |
| Definition idc_from a0 := | |
| exists f : nat -> A, f 0 = a0 /\ forall n, R (f (S n)) (f n). |