LProp
Require Import internalize_tac.
Definition prop_enc (X:Prop) (x:X):=I.
(* eleminate props *)
Instance register_Prop_el (X:Prop) : registered X.
Proof.
register (@prop_enc X).
Defined.
(*
Instance register_Prop : registered Prop.
Proof.
register (fun (_:Prop) => I).
Defined.
*)
(* this can go away once we have that registered P -> internalized (x : P) *)
Instance prop_term (X:Prop) (x:X): internalized x.
internalizeC (enc x).
Defined.
(*
(*e.g. not*)
Instance prop1_term X (H:registered X) (f:X -> Prop): internalized f.
Proof.
internalizeC (lam (enc I)).
Defined.
(*e.g. and*)
Instance prop2_term X Y (HX:registered X) (HY:registered Y) (f:X -> Y -> Prop): internalized f.
Proof.
internalizeC (lam (lam (enc I))).
Defined.
(*e.g. elem*)
Instance prop3_term X Y Z (HX:registered X) (HY:registered Y) (HY:registered Z) (f:X -> Y -> Z -> Prop): internalized f.
Proof.
internalizeC (lam (lam (lam (enc I)))).
Defined.
*)
Definition prop_enc (X:Prop) (x:X):=I.
(* eleminate props *)
Instance register_Prop_el (X:Prop) : registered X.
Proof.
register (@prop_enc X).
Defined.
(*
Instance register_Prop : registered Prop.
Proof.
register (fun (_:Prop) => I).
Defined.
*)
(* this can go away once we have that registered P -> internalized (x : P) *)
Instance prop_term (X:Prop) (x:X): internalized x.
internalizeC (enc x).
Defined.
(*
(*e.g. not*)
Instance prop1_term X (H:registered X) (f:X -> Prop): internalized f.
Proof.
internalizeC (lam (enc I)).
Defined.
(*e.g. and*)
Instance prop2_term X Y (HX:registered X) (HY:registered Y) (f:X -> Y -> Prop): internalized f.
Proof.
internalizeC (lam (lam (enc I))).
Defined.
(*e.g. elem*)
Instance prop3_term X Y Z (HX:registered X) (HY:registered Y) (HY:registered Z) (f:X -> Y -> Z -> Prop): internalized f.
Proof.
internalizeC (lam (lam (lam (enc I)))).
Defined.
*)