New file

In this file...

Main declarations

• ConNF.foo: Something new.

instance ConNF.instIsTransΛLtWithBotSome [Params] : IsTrans Λ fun (β γ : Λ) => ↑β < ↑γ

instance ConNF.instIsWellFoundedΛLtWithBotSome [Params] : IsWellFounded Λ fun (β γ : Λ) => ↑β < ↑γ

def ConNF.motive [Params] (α : Λ) : Motive α

Equations

• ConNF.motive = ICT.fix ConNF.constructMotive ConNF.constructHypothesis

def ConNF.hypothesis [Params] (α : Λ) : Hypothesis (motive α) fun (β : Λ) (x : ↑β < ↑α) => motive β

Equations

• ConNF.hypothesis = ICT.fix_prop ConNF.constructMotive ConNF.constructHypothesis

theorem ConNF.motive_eq [Params] (α : Λ) : motive α = constructMotive α (fun (β : Λ) (x : ↑β < ↑α) => motive β) fun (β : Λ) (x : ↑β < ↑α) => hypothesis β