proposition: Lemma subenv_refl : reflexive subenv.
proof: Proof. move=> e; rewrite /subenv eqxx !subxx /=. apply/andP; split; first by apply/forall_inP=> *. by apply/existsP; exists ord0; rewrite drop0. Qed.
imports: mathcomp(all_ssreflect) bigmin extra