proposition: Lemma wfs_R_retract {C : category} (w : wfs C) {a b a' b'} {f : a --> b} {f' : a' --> b'} (r : retract f f') (hf : (wfs_R w _ _) f) : (wfs_R w _ _) f'.
proof: Proof. use (wfs_L_retract (opp_wfs w) (opp_retract r)). exact hf. 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