proposition: Lemma tele_fix_unfold : tele_forall_app T P (tele_fix R wf P fn) x = tele_forall_pack T _ fn x (tele_forall_unpack T _ (fun y _ => tele_forall_app T P (tele_fix R wf P fn) y)).
proof: Proof. intros. unfold tele_fix, Subterm.FixWf, Fix. rewrite tele_forall_app_type@{i k l}. destruct (wellfounded x). simpl. apply ap. apply ap. apply funext. intros y. apply funext; intros h. eapply id_trans. 2:{ apply id_sym. apply tele_forall_app_type. } apply ap@{l l}. apply Acc_prop. Defined.
imports: Equations.Type.Loader Equations.Type.Logic Equations.Type.FunctionalExtensionality Equations.Type.WellFounded Equations.Type.DepElim Equations.Type.Subterm Equations.Type.Tactics Equations.Type.FunctionalInduction