Module Ord
Definition my_funcY (x: X) (y: Y): Prop.
rewrite EQ in x. specialize (ORDY x y). apply ORDY.
Defined.
About eq_rect.
About eq_rect_r.
End TMP.
Inductive ord (x0 x1: idx): Prop :=
| ord_intro
(EQLOCAL_IDX: x0.(local_idx) = x1.(local_idx))
(EQORD: x0.(local_ord) ~= x1.(local_ord))
(ORD: x1.(local_ord) (eq_rect x0.(local_idx) id x0.(elem) x1.(local_idx) EQLOCAL_IDX) x1.(elem)).
Theorem wf_ord: well_founded ord.
Proof.
econs;
eauto.
ii.
inv H.
destruct a,
y;
ss.
clarify.
apply JMeq_eq in EQORD.
clarify.
clear_tac.
unfold eq_rect in *.
swapname elem1 elem0.
clear ORD.
clear_tac.
{
pattern elem0.
eapply well_founded_ind;
try eassumption.
ii.
clear_tac.
econs;
eauto.
ii.
destruct y;
ss.
inv H0.
ss.
clarify.
specialize (
H elem0).
unfold eq_rect in *.
specialize (
H ORD).
apply JMeq_eq in EQORD.
clarify.
clear_tac.
generalize proof_irr.
intro IRR.
unfold ClassicalFacts.proof_irrelevance in *.
specialize (
IRR _ wf_local_ord0 wf_local_ord1).
clarify.
}
Qed.
Theorem idx_greatest
(local_idx: Type) (local_ord: local_idx -> local_idx -> Prop)
(WF: well_founded local_ord):
embedded local_ord ord.
Proof.
Program Definition idx_bot: idx := @mk unit bot2 _ tt.
Next Obligation.
econs; eauto. ii; ss. Qed.
Lemma idx_bot_spec
i0
(ORD: ord i0 idx_bot):
False.
Proof.
inv ORD. ss. Qed.
Section LIFT.
Variable index: Type.
Variable order: index -> index -> Prop.
Hypothesis WFORD: well_founded order.
Definition lift_idx (i0: index): idx := (mk WFORD i0).
Lemma lift_idx_spec
i0 i1
(ORD: order i0 i1):
<<ORD: ord i0.(lift_idx) i1.(lift_idx)>>.
Proof.
econs;
eauto.
cbn.
instantiate (1:=
eq_refl).
cbn.
ss. Qed.
Hint Unfold lift_idx.
End LIFT.