Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Using Impredicativity to beat the positivity checker
Inductive T :=
| Var : nat -> T
| App : T -> T -> T.
Inductive S e : Prop :=
| def: forall R, (forall i, R i -> S i) ->
(forall e', R e' -> S (App e e')) -> S e.
Definition def' :
forall e, (forall e', S e' -> S (App e e')) -> S e.
intros e ih; apply (def e S); auto.
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment