Reducing an expression with typeclass arg and projectionio

Stream: new members

[Lucas Silver]

We are trying to use the first order logic library to prove that the parallel postulate is independent of the Tarski axioms. We have hit a snag in reducing the realization function from formulae to lean propositions.

The expression we want to reduce is the following.

(LC &0 &1 &1 &0).realize default (fin.snoc (fin.snoc default x) y)

Does anyone know how to reduce this .realize function into the interpretation of LC applied to some variables already in scope?

[Anne Baanen]

I assume unfold realize does not help?