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 j k}. destruct (wellfounded x). simpl. apply ap. apply ap. funext y. funext h. eapply concat. 2:{ apply inverse. apply tele_forall_app_type. } apply ap@{k k}. apply Acc_prop. Defined.
imports: Equations.HoTT.Loader Equations.HoTT.Logic Equations.HoTT.WellFounded Equations.HoTT.DepElim Equations.HoTT.Tactics Equations.HoTT.FunctionalInduction Equations.HoTT.Subterm HoTT(Basics.Tactics)