- wloss: ∀A:Type. (A → A → CProp) → A → A → CProp;
- wloss_prop: (∀T,P,x,y.P x y = wloss T P x y) ∨ (∀T,P,x,y.P y x = wloss T P x y);
+ wloss: ∀A,B:Type. (A → A → B) → A → A → B;
+ wloss_prop: (∀T,R,P,x,y.P x y = wloss T R P x y) ∨ (∀T,R,P,x,y.P y x = wloss T R P x y);