+let rec leibpatt = function
+ | [] -> NotationPt.UserInput
+ | false::sel -> leibpatt sel
+ | true::sel -> NotationPt.Binder (`Forall, (mk_id "_",
+ Some (mk_appl [NotationPt.Implicit `JustOne
+ ;NotationPt.Implicit `JustOne
+ ;NotationPt.Implicit `JustOne
+ ;NotationPt.UserInput])),
+ leibpatt sel);;
+let rec jmeqpatt = function
+ | [] -> NotationPt.UserInput
+ | false::sel -> jmeqpatt sel
+ | true::sel -> NotationPt.Binder (`Forall, (mk_id "_",
+ Some (mk_appl [NotationPt.Implicit `JustOne
+ ;NotationPt.Implicit `JustOne
+ ;NotationPt.Implicit `JustOne
+ ;NotationPt.UserInput
+ ;NotationPt.UserInput])),
+ jmeqpatt sel);;
+
+let rec mk_arrows ~jmeq xs ys selection target =