Library Continuum.Definability
Section First_Order_Logic.
Context {S : ZF_Structure}.
Inductive Term (n : nat) :=
| const : S → Term n
| var : Fin.t n → Term n.
Arguments var {_} _.
Inductive Formula (n : nat) :=
| exist : Formula n.+1 → Formula n
| and : Formula n → Formula n → Formula n
| not : Formula n → Formula n
| equal : Term n → Term n → Formula n
| is_element : Term n → Term n → Formula n.
Arguments exist {_} _.
Arguments and {_} _ _.
Arguments not {_} _.
Arguments equal {_} _ _.
Arguments is_element {_} _ _.
Definition eval_term {n : nat} (t : Term n) (env : Vector.t S n)
: S :=
match t with
| const _ c ⇒ c
| var x ⇒ env[@x]
end.
Fixpoint eval {n: nat} (ϕ : Formula n) (env : Vector.t S n)
: Prop :=
match ϕ with
| exist ϕ ⇒ ∃ x, eval ϕ (x :: env)
| and ϕ ψ ⇒ eval ϕ env ∧ eval ψ env
| not ϕ ⇒ ¬ eval ϕ env
| equal t1 t2 ⇒ eval_term t1 env = eval_term t2 env
| is_element t1 t2 ⇒ eval_term t1 env ∈ eval_term t2 env
end.
End First_Order_Logic.
Arguments var {_ _} _.
Arguments exist {_ _} _.
Arguments and {_ _} _ _.
Arguments not {_ _} _.
Arguments equal {_ _} _ _.
Arguments is_element {_ _} _ _.
Section Environments.
Context {S : ZF_Structure}.
Fixpoint Env_Type_and_Typed_Env (n : nat) :
{ Env_Type : Type & Env_Type → Type } :=
match n with
| 0 ⇒
existT (fun Env_Type ⇒ Env_Type → Type)
unit
(fun _ ⇒ unit)
| n.+1 ⇒
existT (fun type' ⇒ type' → Type)
{ type' : projT1 (Env_Type_and_Typed_Env n) &
projT2 (Env_Type_and_Typed_Env n) type' → Class_Like }
(fun type ⇒ { env' : projT2 (Env_Type_and_Typed_Env n)
(projT1 type) &
projT2 type env' })
end.
Definition Env_Type (n : nat) : Type :=
projT1 (Env_Type_and_Typed_Env n).
Coercion Typed_Env {n} (type : Env_Type n) : Type :=
projT2 (Env_Type_and_Typed_Env n) type.
Definition env_type_nil : Env_Type 0 :=
tt.
Definition env_type_cons
{n} (type' : Env_Type n) (A : type' → Class_Like) :
Env_Type n.+1 :=
existT _ type' A.
Definition env_type_tail {n} (type : Env_Type n.+1) : Env_Type n :=
projT1 type.
Definition env_type_head {n} (type : Env_Type n.+1) :
env_type_tail type → Class_Like :=
projT2 type.
Definition env_nil : env_type_nil :=
tt.
Definition env_cons
{n} {type' : Env_Type n} (env' : type')
{A : type' → Class_Like} (x : A env') :
Typed_Env (env_type_cons type' A) :=
existT _ env' x.
Definition env_tail
{n} {type : Env_Type n.+1}
(env : type) :
Typed_Env (env_type_tail type) :=
projT1 env.
Definition env_head
{n} {type : Env_Type n.+1}
(env : type) :
env_type_head type (env_tail env) :=
projT2 env.
Global Opaque Env_Type_and_Typed_Env Env_Type Typed_Env.
Global Opaque env_type_nil env_type_cons.
Global Opaque env_nil env_cons env_head env_tail.
Fixpoint erase_types {n : nat} :
∀ {type : Env_Type n}, type → Vector.t S n :=
match n with
| 0 ⇒ fun _ _ ⇒ []
| n.+1 ⇒ fun type env ⇒ (encode (env_head env) : S)
:: erase_types (env_tail env)
end.
End Environments.
Infix ";;" := env_type_cons (at level 61, left associativity).
Section Definability.
Set Universe Polymorphism.
Context {S : ZF_Structure}.
Class Definability_On {n} {type : Env_Type n} (A : type → Type) :=
build_definability {
Is_Definable_In_Env : (∀ env : type, A env) → Type
}.
Existing Class Is_Definable_In_Env.
Arguments Is_Definable_In_Env : simpl never.
Arguments build_definability {_ _ _} _.
Definition definability_on
{n} {type : Env_Type n} (A : type → Type)
{definability : Definability_On A} :=
definability.
Notation Is_Definable x :=
(∀ n (type : Env_Type n), Is_Definable_In_Env (fun _ : type ⇒ x)).
Inductive Is_Env_Reduction :
∀ {n k} {type1 : Env_Type n} {type2 : Env_Type k},
(type1 → type2) → Prop :=
| id_is_env_reduction n (type : Env_Type n) :
Is_Env_Reduction (id : type → type)
| composition_with_env_tail_is_env_reduction
n k (type1 : Env_Type n.+1) (type2 : Env_Type k)
(f : env_type_tail type1 → type2) :
Is_Env_Reduction f →
Is_Env_Reduction (f ∘ env_tail).
Existing Class Is_Env_Reduction.
Record Env_Reduction
{n k} (type1 : Env_Type n) (type2 : Env_Type k) : Type :=
build_env_reduction {
env_reduction_fun :> type1 → type2;
env_reduction_property : Is_Env_Reduction env_reduction_fun
}.
Arguments build_env_reduction {_ _ _ _} _ {_}.
Arguments env_reduction_fun {_ _ _ _} _.
Arguments env_reduction_property {_ _ _ _} _.
Global Existing Instance env_reduction_property.
Definition env_reduction_id
{n} {type : Env_Type n} :
Env_Reduction type type.
Proof. ∃ id. apply id_is_env_reduction. Defined.
Global Instance composition_is_env_reduction
{n1 n2 n3}
{type1 : Env_Type n1}
{type2 : Env_Type n2}
{type3 : Env_Type n3}
{r1 : type1 → type2}
{r2 : type2 → type3} :
Is_Env_Reduction r1 →
Is_Env_Reduction r2 →
Is_Env_Reduction (r2 ∘ r1).
Proof.
Admitted.
Definition compose_env_reductions
{n1 n2 n3}
{type1 : Env_Type n1}
{type2 : Env_Type n2}
{type3 : Env_Type n3}
(r1 : Env_Reduction type2 type3)
(r2 : Env_Reduction type1 type2) :
Env_Reduction type1 type3.
Proof. exact (build_env_reduction (r1 ∘ r2)). Defined.
Ltac combine_env_reductions :=
match goal with
[ |- Is_Definable_In_Env
(fun env : ?type ⇒
?f (env_reduction_fun ?r1 (env_reduction_fun ?r2 ?r3))) ] ⇒
change (Is_Definable_In_Env (f ∘ (compose_env_reductions r1 r2)))
end.
Hint Extern 1 (Is_Definable_In_Env
(fun _ ⇒ _ (env_reduction_fun _ (env_reduction_fun _ _)))) ⇒
combine_env_reductions : typeclass_instances.
Global Instance definability_on_Type {n} (type : Env_Type n) :
Definability_On (fun _ : type ⇒ Type) :=
build_definability
(fun A : type → Type ⇒
{ definability :
∀ n' (type' : Env_Type n'),
∀ r : Env_Reduction type' type,
Definability_On (A ∘ r)
&
∀ n' (type' : Env_Type n'),
∀ r : Env_Reduction type' type,
∀ n'' (type'' : Env_Type n''),
∀ r' : Env_Reduction type'' type',
∀ (x : ∀ env, A (r env)),
Is_Definable_In_Env x →
let definability' :=
definability n'' type'' (compose_env_reductions r r') in
Is_Definable_In_Env (x ∘ r')
}).
Global Instance type_weakening
{n} {type : Env_Type n}
{A : type → Type}
{n'} {type' : Env_Type n'}
(r : Env_Reduction type' type) :
Is_Definable_In_Env A →
Is_Definable_In_Env (A ∘ r).
Admitted.
Definition definability_on_fun_type
{n} {type : Env_Type n}
{A : type → Type}
{B : ∀ env, A env → Type}
(HA : ∀ m (type' : Env_Type m),
∀ r : Env_Reduction type' type,
Definability_On (fun env ⇒ A (r env)))
(HB : ∀ m (type' : Env_Type m),
∀ r : Env_Reduction type' type,
∀ a : ∀ env : type', A (r env),
Definability_On (fun env : type' ⇒ B (r env) (a env))) :
Definability_On (fun env ⇒ ∀ a, B env a) :=
build_definability
(fun f : ∀ env a, B env a ⇒
∀ m (type' : Env_Type m) (r : Env_Reduction type' type),
∀ (a : ∀ env, A (r env)),
∀ Ha : Is_Definable_In_Env a,
Is_Definable_In_Env (fun env ⇒ (f (r env)) (a env))).
Hint Extern 1 (Definability_On (fun _ ⇒ _)) ⇒
eapply @definability_on_fun_type :
typeclass_instances.
Lemma fun_weakening
{n} {type : Env_Type n}
{A : type → Type} {B : ∀ env, A env → Type}
{HA : ∀ m (type' : Env_Type m),
∀ r : Env_Reduction type' type,
Definability_On (A ∘ r)}
{HB : ∀ m (type' : Env_Type m),
∀ r : Env_Reduction type' type,
∀ (x : ∀ env, A (r env)),
Definability_On (fun env : type' ⇒ B (r env) (x env))}
{f : ∀ env, ∀ x : A env, B env x}
{k} {type' : Env_Type k} (r : Env_Reduction type' type) :
Is_Definable_In_Env f →
let HA' := fun l (type'' : Env_Type l)
(r' : Env_Reduction type'' type') ⇒
HA l type'' (compose_env_reductions r r') :
Definability_On (A ∘ r ∘ r') in
let HB' := fun l (type'' : Env_Type l)
(r' : Env_Reduction type'' type')
(x : ∀ env, A (r (r' env))) ⇒
HB l type'' (compose_env_reductions r r') x :
Definability_On
(fun env : type'' ⇒ B (r (r' env)) (x env)) in
Is_Definable_In_Env (f ∘ r).
Proof.
cbn. intros Hf l type'' r'.
exact (Hf l type'' (compose_env_reductions r r')).
Defined.
Ltac apply_fun_weakening :=
match goal with
[ |- Is_Definable_In_Env (?f ∘ (env_reduction_fun ?r)) ] ⇒
match type of f with
∀ env : Typed_Env ?type, ∀ (x : @?A env), @?B env x ⇒
let HA :=
constr:(_ : ∀ n' (type' : Env_Type n')
(r' : Env_Reduction type' type),
Definability_On (A ∘ r')) in
let HB :=
constr:(_ : ∀ n' (type' : Env_Type n')
(r' : Env_Reduction type' type)
(x : ∀ env, A (r' env)),
Definability_On (fun env ⇒ B (r' env) (x env))) in
apply (fun_weakening (HA := HA) (HB := HB) (f := f) r)
end
end.
Hint Extern 2 (Is_Definable_In_Env
(Definability_On := definability_on_fun_type _ _)
(_ ∘ (env_reduction_fun _))) ⇒
apply_fun_weakening : typeclass_instances.
Lemma application_is_definable {n} {type : Env_Type n}
{A : type → Type} {B : ∀ env, A env → Type}
{HA : ∀ m (type' : Env_Type m),
∀ r : Env_Reduction type' type,
Definability_On (A ∘ r)}
{HB : ∀ m (type' : Env_Type m),
∀ r : Env_Reduction type' type,
∀ a : ∀ env : type', A (r env),
Definability_On (fun env : type' ⇒ B _ (a env))}
{f : ∀ env (x : A env), B env x}
(Hf : Is_Definable_In_Env f)
{x : ∀ env, A env}
(Hx :
let HA' := HA n type env_reduction_id : Definability_On A in
Is_Definable_In_Env x) :
let HB' := HB n type env_reduction_id x :
Definability_On (fun env ⇒ (B env) (x env)) in
Is_Definable_In_Env (fun env ⇒ f env (x env)).
Proof. intros HB'. apply (Hf n type env_reduction_id). assumption. Defined.
Ltac prove_that_application_is_definable :=
match goal with
[ |- Is_Definable_In_Env (fun env : Typed_Env ?type ⇒ ?f ?y) ] ⇒
match type of (fun env : type ⇒ f) with
∀ env, ∀ a : @?A env, @?B env a ⇒
lazymatch A with
| (fun _ ⇒ Typed_Env _) ⇒ fail
| _ ⇒
let HA := constr:(
_ : ∀ n' (type' : Env_Type n')
(r : Env_Reduction type' type),
Definability_On (A ∘ r))
in
let HB := constr:(
_ : ∀ n' (type' : Env_Type n')
(r : Env_Reduction type' type)
(a : ∀ env, A (r env)),
Definability_On (fun env ⇒ (B (r env)) (a env)))
in notypeclasses refine (application_is_definable
(HA := HA)
(HB := HB)
(f := fun env : type ⇒ f)
_
(x := fun env : type ⇒ y)
_);
cbn
end
end
end.
Hint Extern 100 (Is_Definable_In_Env (fun _ ⇒ _ _)) ⇒
prove_that_application_is_definable : typeclass_instances.
Global Instance lambda_is_definable
{n} {type : Env_Type n}
{A : type → Type}
{HA : ∀ m (type' : Env_Type m),
∀ r : Env_Reduction type' type,
Definability_On (A ∘ r)}
{B : ∀ env, A env → Type}
{HB : ∀ m (type' : Env_Type m),
∀ r : Env_Reduction type' type,
∀ a : ∀ env : type', A (r env),
Definability_On (fun env : type' ⇒ B (r env) (a env))}
{f : ∀ env a, B env a} :
(∀ m (type' : Env_Type m) (r : Env_Reduction type' type),
∀ (x : ∀ env, A (r env))
(Hx : Is_Definable_In_Env x),
Is_Definable_In_Env (fun env ⇒ (f (r env)) (x env))) →
Is_Definable_In_Env (fun env x ⇒ f env x).
Admitted.
Global Instance definability_on_Prop
{n} (type : Env_Type n) :
Definability_On (fun _ : type ⇒ Prop)
| 100 :=
build_definability
(fun P : type → Prop ⇒
{ ϕ : Formula n |
∀ env, P env ↔ eval ϕ (erase_types env) }).
Global Instance Prop_weakening
{n} {type : Env_Type n}
{n'} {type' : Env_Type n'}
{P : type → Prop}
(r : Env_Reduction type' type) :
Is_Definable_In_Env P →
Is_Definable_In_Env (P ∘ r).
Admitted.
Global Instance definability_on_type_with_encoding
{n} {type : Env_Type n}
{A : type → Type}
(encoding : ∀ env, Encoding_Of (A env)) :
Definability_On A | 10 :=
build_definability
(fun x ⇒ { f : Formula n.+1 &
∀ x' env, eval f (x' :: erase_types env) ↔
x' = encode (x env) }).
Lemma weakening_on_type_with_encoding
{n} {type : Env_Type n} {A : type → Type}
(encodings : ∀ env, Encoding_Of (A env))
{n'} {type' : Env_Type n'}
(x : ∀ env, A env) (r : Env_Reduction type' type) :
Is_Definable_In_Env x →
Is_Definable_In_Env
(Definability_On := definability_on_type_with_encoding (encodings ∘ r))
(x ∘ r).
Admitted.
Ltac apply_weakening_on_type_with_encoding :=
match goal with
[ |- Is_Definable_In_Env
(Definability_On := definability_on_type_with_encoding _)
(?y ∘ env_reduction_fun ?r) ] ⇒
match type of y with
∀ env : ?type, @?A env ⇒
let H := constr:(_ : ∀ env : type, Encoding_Of (A env)) in
notypeclasses refine (weakening_on_type_with_encoding H y r _)
end
end.
Hint Extern 5 (Is_Definable_In_Env
(Definability_On := definability_on_type_with_encoding _)
(_ ∘ env_reduction_fun _)) ⇒
apply_weakening_on_type_with_encoding : typeclass_instances.
Goal Is_Definable (fun (x : S) (f : S → S) ⇒ f x).
exact _.
Qed.
Global Instance encode_is_definable (A : Type) (H : Encoding_Of A) :
Is_Definable (encode : A → encoding_of A).
Admitted.
Global Instance constant_element_is_definable
{n} {type : Env_Type n}
{A : Class_Like} (x : A) :
Is_Definable_In_Env (fun _ : type ⇒ x).
Admitted.
Global Instance element_value_is_definable (C : Class) :
Is_Definable (element_value : C → S).
Admitted.
Global Instance element_is_definable
{n} {type : Env_Type n}
(C : type → Class) (x : ∀ env, S) (Hx : ∀ env, x env ∈ C env) :
Is_Definable_In_Env x →
Is_Definable_In_Env (fun env ⇒ element (x env) : C env).
Admitted.
Global Instance definability_on_Class {n} (type : Env_Type n) :
Definability_On (fun _ : type ⇒ Class) :=
build_definability
(fun A ⇒ Is_Definable_In_Env (fun env ⇒ fun x : S ⇒ x ∈ A env)).
Global Instance Class_weakening
{n} {type : Env_Type n}
{n'} {type' : Env_Type n'}
{C : type → Class}
(r : Env_Reduction type' type) :
Is_Definable_In_Env C →
Is_Definable_In_Env (C ∘ r).
Admitted.
Global Instance set_as_class_is_definable :
Is_Definable set_as_class.
Admitted.
Global Instance definability_on_Encoding
{n} {type : Env_Type n}
(A : type → Type) :
Definability_On (fun env ⇒ Encoding_Of (A env)) :=
build_definability
(fun encoding : ∀ env, Encoding_Of (A env) ⇒
Is_Definable_In_Env (encoding : type → Class)).
Global Instance Encoding_weakening
{n} {type : Env_Type n}
{n'} {type' : Env_Type n'}
{A : type → Type}
{E : ∀ env, Encoding_Of (A env)}
(r : Env_Reduction type' type) :
Is_Definable_In_Env E →
Is_Definable_In_Env (E ∘ r).
Admitted.
Global Instance encoding_of_the_universe_is_definable :
Is_Definable encoding_of_the_universe.
Admitted.
Global Instance encoding_of_class_is_definable :
Is_Definable encoding_of_class.
Admitted.
Global Instance definability_on_Class_Like {n} (type : Env_Type n) :
Definability_On (fun _ : type ⇒ Class_Like) :=
build_definability
(fun x ⇒ Is_Definable_In_Env (fun env ⇒ class_like_encoding (x env))).
Global Instance Class_Like_weakening
{n} {type : Env_Type n}
{n'} {type' : Env_Type n'}
{C : type → Class_Like}
(r : Env_Reduction type' type) :
Is_Definable_In_Env C →
Is_Definable_In_Env (C ∘ r).
Admitted.
Global Instance definability_on_constant_definability
{n} (type : Env_Type n)
(A : type → Type)
(H : ∀ env n (type' : Env_Type n),
Definability_On (fun _ : type' ⇒ A env))
(x : ∀ env, A env) :
Definability_On (fun env ⇒ Is_Definable (x env)).
Admitted.
Global Instance definability_proof_is_definable
{n} (type : Env_Type n)
(A : type → Type)
(H : ∀ env n (type' : Env_Type n),
Definability_On (fun _ : type' ⇒ A env))
(x : ∀ env, A env)
(d : ∀ env, Is_Definable (x env)) :
Is_Definable_In_Env d.
Admitted.
Goal Is_Definable (fun (x : S) (f : ∀ x : S, x) ⇒ f x).
Proof. exact _. Qed.
Global Instance True_is_definable :
Is_Definable True.
Admitted.
Global Instance False_is_definable :
Is_Definable False.
Admitted.
Global Instance not_is_definable :
Is_Definable Logic.not.
Admitted.
Global Instance and_is_definable :
Is_Definable Logic.and.
Admitted.
Global Instance or_definable :
Is_Definable or.
Admitted.
Global Instance impl_is_definable
{n} {type : Env_Type n}
(P Q : type → Prop) :
Is_Definable_In_Env P →
Is_Definable_In_Env Q →
Is_Definable_In_Env (fun env ⇒ P env → Q env).
Admitted.
Global Instance ex_statement_is_definable
{n} {type : Env_Type n}
{A : type → Type}
{E : ∀ env, Encoding_Of (A env)}
{P : ∀ env, A env → Prop} :
Is_Definable_In_Env E →
Is_Definable_In_Env P →
Is_Definable_In_Env (fun env ⇒ ∃ x : A env, P env x).
Admitted.
Hint Extern 1 (Is_Definable_In_Env (fun _ ⇒ ∃ _, _)) ⇒
simple notypeclasses refine (ex_statement_is_definable _ _)
: typeclass_instances.
Global Instance forall_statement_is_definable
{n} {type : Env_Type n}
{A : type → Type}
{E : ∀ env, Encoding_Of (A env)}
{P : ∀ env, A env → Prop} :
Is_Definable_In_Env E →
Is_Definable_In_Env P →
Is_Definable_In_Env (fun env ⇒ ∀ x : A env, P env x).
Admitted.
Hint Extern 1 (Is_Definable_In_Env (fun _ ⇒ ∀ _, _)) ⇒
simple notypeclasses refine (forall_statement_is_definable _ _)
: typeclass_instances.
Global Instance equality_is_definable (A : Class_Like) :
Is_Definable (eq : A → A → Prop).
Admitted.
Global Instance element_relation_is_definable :
Is_Definable element_relation.
Admitted.
End Definability.
Arguments encoding_of {_} _ {_}.
Arguments Is_Definable_In_Env : simpl never.
About build_env_reduction.
Arguments build_env_reduction {_ _ _ _ _} _ {_}.
Arguments env_reduction_fun {_ _ _ _ _} _.
Arguments env_reduction_property {_ _ _ _ _} _.
Notation Is_Definable x :=
(∀ n (type : Env_Type n), Is_Definable_In_Env (fun _ : type ⇒ x)).
Hint Extern 1 (Definability_On (fun _ ⇒ _)) ⇒
eapply @definability_on_fun_type :
typeclass_instances.
Ltac prove_that_application_is_definable :=
match goal with
[ |- Is_Definable_In_Env (fun env : Typed_Env ?type ⇒ ?f ?y) ] ⇒
match type of (fun env : type ⇒ f) with
∀ env, ∀ a : @?A env, @?B env a ⇒
lazymatch A with
| (fun _ ⇒ Typed_Env _) ⇒ fail
| _ ⇒
let HA := constr:(
_ : ∀ n' (type' : Env_Type n')
(r : Env_Reduction type' type),
Definability_On (A ∘ r))
in
let HB := constr:(
_ : ∀ n' (type' : Env_Type n')
(r : Env_Reduction type' type)
(a : ∀ env, A (r env)),
Definability_On (fun env ⇒ (B (r env)) (a env)))
in notypeclasses refine (application_is_definable
(HA := HA)
(HB := HB)
(f := fun env : type ⇒ f)
_
(x := fun env : type ⇒ y)
_);
cbn
end
end
end.
Hint Extern 50 (Is_Definable_In_Env (fun _ ⇒ _ _)) ⇒
prove_that_application_is_definable : typeclass_instances.
Ltac apply_fun_weakening :=
match goal with
[ |- Is_Definable_In_Env (?f ∘ (env_reduction_fun ?r)) ] ⇒
match type of f with
∀ env : Typed_Env ?type, ∀ (x : @?A env), @?B env x ⇒
let HB :=
constr:(_ : ∀ n' (type' : Env_Type n')
(r' : Env_Reduction type' type)
(x : ∀ env, A (r' env)),
Is_Definable_In_Env x →
Definability_On (fun env ⇒ B (r' env) (x env))) in
apply (fun_weakening (f := f) (HB := HB))
end
end.
Hint Extern 2 (Is_Definable_In_Env (_ ∘ (env_reduction_fun _))) ⇒
apply_fun_weakening : typeclass_instances.
Ltac combine_env_reductions :=
match goal with
[ |- Is_Definable_In_Env
(fun env : ?type ⇒
?f (env_reduction_fun ?r1 (env_reduction_fun ?r2 ?r3))) ] ⇒
change (Is_Definable_In_Env (f ∘ (compose_env_reductions r1 r2)))
end.
Hint Extern 2 (Is_Definable_In_Env (fun _ ⇒ _ (_ _))) ⇒
combine_env_reductions : typeclass_instances.
Ltac apply_weakening_on_type_with_encoding :=
match goal with
[ |- Is_Definable_In_Env
(Definability_On := definability_on_type_with_encoding _)
(?y ∘ env_reduction_fun ?r) ] ⇒
match type of y with
∀ env : ?type, @?A env ⇒
let H := constr:(_ : ∀ env : type, Encoding_Of (A env)) in
notypeclasses refine (weakening_on_type_with_encoding H y r _)
end
end.
Hint Extern 5 (Is_Definable_In_Env
(Definability_On := definability_on_type_with_encoding _)
(_ ∘ env_reduction_fun _)) ⇒
apply_weakening_on_type_with_encoding : typeclass_instances.
Hint Extern 1 (Is_Definable_In_Env (fun _ ⇒ ∃ _, _)) ⇒
simple notypeclasses refine (ex_statement_is_definable _ _)
: typeclass_instances.
Hint Extern 1 (Is_Definable_In_Env (fun _ ⇒ ∀ _, _)) ⇒
simple notypeclasses refine (forall_statement_is_definable _ _)
: typeclass_instances.