proposition: Lemma wfs_wf_wfp_desc (f : nat -> wfs) (b : forall n : nat, wfs_wf_uord (f (S n)) (f n)) : ∏ n : nat, uord (f 0) (wfs_wf_wfp_seq f b (S n)) (wfs_wf_wfp_seq f b n).
proof: Proof. intro n. exact (wfs_wf_wfp_compshift f b n (domicom (b n) (domi (b (S n))))). Defined.
imports: UniMath.Foundations.All UniMath.Tactics.EnsureStructuredProofs