proposition: Lemma abstract_context T (P : T -> Type) x : (forall Q, Q = P -> Q x) -> P x.
proof: Proof. by move=> /(_ P); apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching