New file

In this file...

Main declarations

• ConNF.foo: Something new.

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

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

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

Equations

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

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

Equations

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

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