proposition: Lemma linearly_extendable : forall R, rel_midex R -> (eq_midex A /\ irreflexive (clos_trans R) <-> forall l, exists R', linear_extension R l R' /\ rel_midex R').
proof: Proof. unfold linear_extension. split; intros. exists (LETS R l). split. split. apply LETS_restricted. split. apply LETS_sub_rel. split. apply LETS_transitive. split. destruct (LETS_irrefl R l). tauto. apply H1. apply irreflexive_incl with (clos_trans R). unfold inclusion. apply tc_incl. apply incl_restriction. tauto. apply LETS_total; tauto. apply LETS_midex; tauto. split. apply total_order_eq_midex. intro. destruct (H0 l). exists x. tauto. apply local_global_acyclic. intro. destruct (H0 l). exists x. tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)