ghost_cic.lean

-- imagine pseudo terms like this
-- def id : Pi (A : Type), A -> A := ...

-- irrelevant.fun 
irrelevant.fun A Type (fun x, x)

-- irrelevant.fun A Type (fun x, x) => fun x, x

-- application of id
(irrelevant.app (fun x, x) A) 10

-- rule for compilation later on strips type information simply by
-- (irrelevant.app (fun x, x) A) 10 => (fun x, x) 10

-- eq.rec
(irrelevant.eq_rec A C a) (irrelevant.fun a1 A (irrelvant.fun equality (a = a1) term))
-- (irrelevant.eq_rec A C a) (irrelevant.fun a1 A (irrelvant.fun equality (a = a1) term)) => term

-- essentially just keep these extra annotations around until the last level compilation where we strip them
-- and emit bytecode like normal