Lemma toBranch_hsubtype {T : preZFS} {x : T} {S : hsubtype (pr111 T)} {t : pr111 T} (e : Ed T x t) (s : S t) : hsubtype_to_preZFS_Branch_hsubtype T x S (t ,, e). Proof. unfold hsubtype_to_preZFS_Branch_hsubtype. simpl. split. apply s. apply e. Qed.