+ (λw.(f x (w x) = f x (w y))) (λw:P.hole ? w).
+*)
+
+(* meta Vs term && term Vs meta with different local ctx
+axiom foo:
+ ∀P:Type.∀f:P→P→P.∀x,y:P.
+ (λw.(f (w x) (hole ? x) = f x (w y))) (λw:P.hole ? w).
+*)
+
+(* occur check
+axiom foo:
+ ∀P:Type.∀f:P→P→P.∀x,y:P.
+ (λw.(f x (f (w x) x) = f x (w y))) (λw:P.hole ? w).
+*)
+
+(* unifying the type of (y ?) with (Q x) we instantiate ? to x
+axiom foo:
+ ∀P:Type.∀Q:P→Type.∀f:∀x:P.Q x→P→P.∀x:P.∀y:∀x.Q x.
+ (λw.(f w (y w) x = (id ? f) x (hole ? (y x)) x)) (hole ? x).
+*)
+
+alias num (instance 0) = "natural number".
+axiom foo: (100+111) = (100+110).
+
+
+ (id ?(id ?(id ?(id ? (100+100))))) =
+ (id ?(id ?(id ?(id ? (99+100))))).[3:
+ apply (refl_eq nat (id ?(id ?(id ?(id ? (98+102+?))))));