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 poly_f_equal@{k k}. apply poly_f_equal@{k k}. extensionality y. extensionality h. rewrite tele_forall_app_type@{i j k}. apply poly_f_equal@{k k}. apply Subterm.Acc_pi. Defined.
imports: Equations.Prop.Loader Coq(FunctionalExtensionality) Equations.Prop.DepElim Equations.Prop.Tactics Equations.Prop.FunctionalInduction