proposition: Lemma wfs'lp (w : wfs C) {x y a b} {f : x --> y} {g : a --> b} (hf : (wfs_L w _ _) f) (hg : (wfs_R w _ _) g) : lp f g.
proof: Proof. unfold wfs_L in hf. rewrite (wfs_llp w) in hf. exact (hf _ _ _ hg). Qed.
imports: UniMath.MoreFoundations.All UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.ModelCategories.Retract UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Lifting