proposition: Lemma mixed_ind : forall I A B (E:binary B) (M:family I B) (P:A->Prop) (F:(A->B)->(A->B)) (R:binary A) (S:I->A->B->Prop) (f:A->B), (forall x, P x -> E (f x) (F f x)) -> E = similar M -> COFE M -> wf R -> mixed_continuous M S -> (forall i x, (forall j y, P y -> lexico2 (family_r M) R (j,y) (i,x) -> S j y (f y)) -> S i x (F f x)) -> (forall i x, P x -> S i x (f x)).
proof: Proof. Proof using. introv Eqf Equiv Cofe Wfr Cont Inv. intros i x. sets_eq p: (i, x). gen i x. induction_wf IH: (wf_lexico2 (ofe_wf Cofe) (wf_tclosure Wfr)) p. intros i x Eix. destruct p. inversions Eix. intros Px. eapply Cont with (y1 := F f x). apply Inv. intros. apply* IH. forwards*: (>> rel_incl_lexico2 I A (family_r M) (family_r M) R (tclosure R) (j,y) (i,x)). intros. apply~ equiv_sym. apply~ Eqf. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)