proposition: Lemma href_translation C : ref F C -> href C.
proof: Proof. Proof using sfc_F. elim => {C}; eauto using coref_supp,ax_ReqR. - move => S C sub0 _ coS inS. case/hasP => [[[]//[]// s t [|] //]] inC. exact: unfulfilledAR_refute. - move => S C sub0 _ coS inS. case/hasP => [[[]//[]// s t [|] //]] inC. exact: unfulfilledAU_refute. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.CTL(CTL_def dags demo hilbert relaxed_pruning)