module ReflexiveTransitiveClosure where data _* {A : Set} (R : A → A → Set) : A → A → Set where r : (a : A) → (R *) a a i : (a a' : A) → R a a' → (R *) a a' t : (a a' a'' : A) → (R *) a a' → (R *) a' a'' → (R *) a a'' {- Now we can implement proof by "rule induction": -} *-induction : {A : Set} → {R Q : A → A → Set} → ((a : A) → Q a a) → ((a a' : A) → R a a' → Q a a') → ((a a' a'' : A) → Q a a' → Q a' a'' → Q a a'') → (a a' : A) → (R *) a a' → Q a a' *-induction q-refl q-inj q-trans a .a (r .a) = q-refl a *-induction q-refl q-inj q-trans a a' (i .a .a' p) = q-inj a a' p *-induction q-refl q-inj q-trans a a'' (t .a a' .a'' p q) = q-trans a a' a'' (*-induction q-refl q-inj q-trans a a' p) (*-induction q-refl q-inj q-trans a' a'' q)