phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/streams.v *)
CoInductive stream_equiv' {A} (s1 s2 : stream A) : Prop
:=
  scons_equiv' :
    shead s1 = shead s2 → stream_equiv' (stail s1) (stail s2) →
    stream_equiv' s1 s2.
(* stdpp/streams.v *)
Instance stream_equiv {A} : Equiv (stream A)
:= stream_equiv'.
(* stdpp/streams.v *)
Fixpoint slookup {A} (i : nat) (s : stream A) : A
:=
  match i with O => shead s | S i => stail s !.! i end
where "s !.! i" := (slookup i s).
(* stdpp/streams.v *)
Instance stream_fmap : FMap stream
:= λ A B f,
  cofix go s := f (shead s) :.: go (stail s).
(* stdpp/streams.v *)
Fixpoint stake {A} (n : nat) (s : stream A)
:=
  match n with 0 => [] | S n => shead s :: stake n (stail s) end.
(* stdpp/streams.v *)
CoFixpoint srepeat {A} (x : A) : stream A
:= x :.: srepeat x.
(* stdpp/streams.v *)
Lemma scons_equiv s1 s2 : shead s1 = shead s2 → stail s1 ≡ stail s2 → s1 ≡ s2.
Proof. by constructor. Qed.
(* stdpp/streams.v *)
Instance equal_equivalence : Equivalence (≡@{stream A}).
Proof.
  split.
  - now cofix FIX; intros ?; constructor.
  - now cofix FIX; intros ?? [??]; constructor.
  - cofix FIX; intros ??? [??] [??]; constructor; etrans; eauto.
Qed.
(* stdpp/streams.v *)
Instance scons_proper x : Proper ((≡) ==> (≡)) (scons x).
Proof. by constructor. Qed.
(* stdpp/streams.v *)
Instance shead_proper : Proper ((≡) ==> (=@{A})) shead.
Proof. by intros ?? [??]. Qed.
(* stdpp/streams.v *)
Instance stail_proper : Proper ((≡) ==> (≡@{stream A})) stail.
Proof. by intros ?? [??]. Qed.
(* stdpp/streams.v *)
Instance slookup_proper i : Proper ((≡@{stream A}) ==> (=)) (slookup i).
Proof. by induction i as [|i IH]; intros s1 s2 Hs; simpl; rewrite Hs. Qed.
(* stdpp/stringmap.v *)
Notation stringmap
:= (gmap string).
(* stdpp/stringmap.v *)
Notation stringset
:= (gset string).
(* stdpp/stringmap.v *)
Let R {A} (s : string) (m : stringmap A) (n1 n2 : N)
:=
  n2 < n1 ∧ is_Some (m !! (s +:+ pretty (n1 - 1))).
(* stdpp/stringmap.v *)
Lemma fresh_string_step {A} s (m : stringmap A) n x :
  m !! (s +:+ pretty n) = Some x → R s m (1 + n) n.
Proof. split; [lia|]. replace (1 + n - 1) with n by lia; eauto. Qed.
(* stdpp/stringmap.v *)
Lemma fresh_string_R_wf {A} s (m : stringmap A) : well_founded (R s m).
Proof.
  induction (map_wf m) as [m _ IH]. intros n1; constructor; intros n2 [Hn Hs].
  specialize (IH _ (delete_subset m (s +:+ pretty (n2 - 1)) Hs) n2).
  cut (n2 - 1 < n2); [|lia]. clear n1 Hn Hs; revert IH; generalize (n2 - 1).
  intros n1. induction 1 as [n2 _ IH]; constructor; intros n3 [??].
  apply IH; [|lia]; split; [lia|].
  by rewrite lookup_delete_ne by (intros ?; simplify_eq/=; lia).
Qed.
(* stdpp/stringmap.v *)
Definition fresh_string_go {A} (s : string) (m : stringmap A) (n : N)
    (go : ∀ n', R s m n' n → string) : string
:=
  let s' := s +:+ pretty n in
  match Some_dec (m !! s') with
  | inleft (_↾Hs') => go (1 + n)%N (fresh_string_step s m n _ Hs')
  | inright _ => s'
  end.
(* stdpp/stringmap.v *)
Definition fresh_string {A} (s : string) (m : stringmap A) : string
:=
  match m !! s with
  | None => s
  | Some _ =>
     Fix_F _ (fresh_string_go s m) (wf_guard 32 (fresh_string_R_wf s m) 0)
  end.
(* stdpp/stringmap.v *)
Lemma fresh_string_fresh {A} (m : stringmap A) s : m !! fresh_string s m = None.
Proof.
  unfold fresh_string. destruct (m !! s) as [a|] eqn:Hs; [clear a Hs|done].
  generalize 0 (wf_guard 32 (fresh_string_R_wf s m) 0); revert m.
  fix FIX 3; intros m n [?]; simpl; unfold fresh_string_go at 1; simpl.
  destruct (Some_dec (m !! _)) as [[??]|?]; auto.
Qed.
(* stdpp/stringmap.v *)
Definition fresh_string_of_set (s : string) (X : stringset) : string
:=
  fresh_string s (mapset.mapset_car X).
(* stdpp/stringmap.v *)
Lemma fresh_string_of_set_fresh (X : stringset) s : fresh_string_of_set s X ∉ X.
Proof. apply eq_None_ne_Some, fresh_string_fresh. Qed.
(* stdpp/stringmap.v *)
Fixpoint fresh_strings_of_set
    (s : string) (n : nat) (X : stringset) : list string
:=
  match n with
  | 0 => []
  | S n =>
     let x := fresh_string_of_set s X in
     x :: fresh_strings_of_set s n ({[ x ]} ∪ X)
  end%nat.
(* stdpp/strings.v *)
(* The [Countable] instance of [string] is particularly useful to allow strings
to be used as keys in [gmap].

The encoding of [string] to [positive] is taken from
https://github.com/xavierleroy/canonical-binary-tries/blob/v2/lib/String2pos.v.
It avoids creating auxiliary data structures such as [list bool], thereby
improving efficiency.

We first provide some [Local] helper functions and then define the [Countable]
instances for encoding/decoding in the modules [Ascii] and [String]. End-users
should always use these instances. *)
Definition bool_cons_pos (b : bool) (p : positive) : positive
:=
  if b then p~1 else p~0.
(* stdpp/strings.v *)
Definition ascii_cons_pos (c : ascii) (p : positive) : positive
:=
  match c with
  | Ascii b0 b1 b2 b3 b4 b5 b6 b7 =>
     bool_cons_pos b0 $ bool_cons_pos b1 $ bool_cons_pos b2 $
       bool_cons_pos b3 $ bool_cons_pos b4 $ bool_cons_pos b5 $
       bool_cons_pos b6 $ bool_cons_pos b7 p
  end.
(* stdpp/strings.v *)
Fixpoint string_to_pos (s : string) : positive
:=
  match s with
  | EmptyString => 1
  | String c s => ascii_cons_pos c (string_to_pos s)
  end.
(* stdpp/strings.v *)
(* The decoder that turns [positive] into string results in 256 cases (we need
to peel off 8 times a [~0]/[~1] constructor) and a number of fall through cases.
We avoid writing these cases explicitly by generating the definition using Ltac.
The lemma [string_of_to_pos] ensures the generated definition is correct.

Alternatively, we could implement it in two steps. Convert the [positive] to
[list bool], and convert the list to [string]. This definition will be slower
since auxiliary data structures are created. *)
Fixpoint pos_to_string (p : positive) : string.
Proof.
  (** The argument [p] is the [positive] that we are peeling off.
  The argument [a] is the constructor [Ascii] partially applied to some number
  of Booleans (so its Coq type changes during the iteration).
  The argument [n] says how many more Booleans are needed to make this fully
  applied so that the [constr] has type ascii. *)
  let rec gen p a n :=
    lazymatch n with
    (* This character is done. Stop the ltac recursion; recursively invoke
    [pos_to_string] on the Gallina level for the remaining bits. *)
    | 0 => exact (String a (pos_to_string p))
    (* There are more bits to consume for this character, generate an
    appropriate [match] with ltac. *)
    | S ?n =>
       exact (match p with
              | 1 => EmptyString
              | p~0 => ltac:(gen p (a false) n)
              | p~1 => ltac:(gen p (a true) n)
              end%positive)
    end in
  gen p Ascii 8.
Defined.
(* stdpp/strings.v *)
Lemma pos_to_string_string_to_pos s : pos_to_string (string_to_pos s) = s.
Proof. induction s as [|[[][][][][][][][]]]; by f_equal/=. Qed.
(* stdpp/strings.v *)
Instance eq_dec : EqDecision ascii
:= ascii_dec.
(* stdpp/strings.v *)
Instance countable : Countable ascii := {|
    encode a := string_to_pos (String a EmptyString);
    decode p := match pos_to_string p return _ with String a _ => Some a | _ => None end
  |}.
Next Obligation. by intros [[] [] [] [] [] [] [] []]. Qed.
(* stdpp/strings.v *)
Definition is_nat (x : ascii) : option nat
:=
    match x with
    | "0" => Some 0
    | "1" => Some 1
    | "2" => Some 2
    | "3" => Some 3
    | "4" => Some 4
    | "5" => Some 5
    | "6" => Some 6
    | "7" => Some 7
    | "8" => Some 8
    | "9" => Some 9
    | _ => None
    end%char.
(* stdpp/strings.v *)
Definition is_space (x : ascii) : bool
:=
    match x with
    | "009" | "010" | "011" | "012" | "013" | " " => true | _ => false
    end%char.
(* stdpp/strings.v *)
(* Use a name that is consistent with [list]. [only parsing] because it looks
  like starting with Rocq 9.2, notations in modules that are not imported are
  anyway not used for printing. *)
Notation app
:= String.append (only parsing).
(* stdpp/strings.v *)
Instance eq_dec : EqDecision string.
Proof. solve_decision. Defined.
(* stdpp/strings.v *)
Instance inhabited : Inhabited string
:= populate "".
(* stdpp/strings.v *)
Instance countable : Countable string
:= {|
    encode := string_to_pos;
    decode p := Some (pos_to_string p)
  |}.
(* stdpp/strings.v *)
Definition le (s1 s2 : string) : Prop
:= String.leb s1 s2.
(* stdpp/strings.v *)
Instance le_dec : RelDecision le.
Proof. intros s1 s2. apply _. Defined.
(* stdpp/strings.v *)
Instance le_pi s1 s2 : ProofIrrel (le s1 s2).
Proof. apply _. Qed.
(* stdpp/strings.v *)
Instance le_po : PartialOrder le.
Proof.
    unfold le. split; [split|].
    - intros s. unfold String.leb. assert ((s ?= s)%string = Eq) as ->; [|done].
      induction s; simpl; [done|].
      unfold Ascii.compare. by rewrite N.compare_refl.
    - intros s1 s2 s3. unfold String.leb.
      destruct (s1 ?= s2)%string eqn:Hs12; [..|done].
      { by apply String.compare_eq_iff in Hs12 as ->. }
      destruct (s2 ?= s3)%string eqn:Hs23; [..|done].
      { apply String.compare_eq_iff in Hs23 as ->. by rewrite Hs12. }
      assert ((s1 ?= s3)%string = Lt) as ->; [|done].
      revert s2 s3 Hs12 Hs23.
      induction s1 as [|a1 s1]; intros [|a2 s2] [|a3 s3] ??;
        simplify_eq/=; [done..|].
      destruct (Ascii.compare a1 a2) eqn:Ha12; simplify_eq/=.
      { apply Ascii.compare_eq_iff in Ha12 as ->.
        destruct (Ascii.compare a2 a3); simpl; eauto. }
      destruct (Ascii.compare a2 a3) eqn:Ha23; simplify_eq/=.
      { apply Ascii.compare_eq_iff in Ha23 as ->. by rewrite Ha12. }
      assert (Ascii.compare a1 a3 = Lt) as ->; [|done].
      apply N.compare_lt_iff. by etrans; apply N.compare_lt_iff.
    - intros s1 s2 ?%Is_true_true ?%Is_true_true. by apply String.leb_antisym.
  Qed.
(* stdpp/strings.v *)
Instance le_total : Total le.
Proof.
    intros s1 s2. unfold le. destruct (String.leb_total s1 s2) as [->| ->]; auto.
  Qed.
(* stdpp/strings.v *)
Instance app_inj s1 : Inj (=) (=) (app s1).
Proof. intros ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
(* stdpp/strings.v *)
Fixpoint rev_app (s1 s2 : string) : string
:=
    match s1 with
    | "" => s2
    | String a s1 => rev_app s1 (String a s2)
    end.
(* stdpp/strings.v *)
Definition rev (s : string) : string
:= rev_app s "".
(* stdpp/strings.v *)
(* Break a string up into lists of words, delimited by white space *)
Fixpoint words_go (cur : option string) (s : string) : list string
:=
    match s with
    | "" => option_list (rev <$> cur)
    | String a s =>
       if Ascii.is_space a
       then option_list (rev <$> cur) ++ words_go None s
       else words_go (Some (from_option (String a) (String a "") cur)) s
    end.
(* stdpp/strings.v *)
Definition words : string → list string
:= words_go None.
(* stdpp/strings.v *)
Ltac words s
:=
    match type of s with
    | list string => s
    | string => eval vm_compute in (words s)
    end.
(* stdpp/strings.v *)
Notation "(≤)"
:= String.le (only parsing) : string_scope.
(* stdpp/strings.v *)
Notation "x ≤ y ≤ z"
:= (x ≤ y ∧ y ≤ z)%string : string_scope.
(* stdpp/strings.v *)
Notation "x ≤ y ≤ z ≤ z'"
:= (x ≤ y ∧ y ≤ z ∧ z ≤ z')%string : string_scope.
(* stdpp/tactics.v *)
Lemma f_equal_dep {A B} (f g : ∀ x : A, B x) x : f = g → f x = g x.
Proof. intros ->; reflexivity. Qed.
(* stdpp/tactics.v *)
Lemma f_equal_help {A B} (f g : A → B) x y : f = g → x = y → f x = g y.
Proof. intros -> ->; reflexivity. Qed.
(* stdpp/tactics.v *)
Ltac f_equal
:=
  let rec go :=
    match goal with
    | _ => reflexivity
    | _ => apply f_equal_help; [go|try reflexivity]
    | |- ?f ?x = ?g ?x => apply (f_equal_dep f g); go
    end in
  try go.
(* stdpp/tactics.v *)
(* The tactic [intuition] expands to [intuition auto with *] by default. This
is rather inefficient when having big hint databases, or expensive [Hint Extern]
declarations as the ones above. *)
Ltac intuition_solver :
:= auto.
(* stdpp/tactics.v *)
(* The [fast_reflexivity] tactic only works on syntactically equal terms. It
can be used to avoid expensive failing unification. *)
Ltac fast_reflexivity
:=
  match goal with
  | |- _ ?x ?x => solve [simple apply reflexivity]
  end.
(* stdpp/tactics.v *)
(* [done] can get slow as it calls "trivial". [fast_done] can solve way less
goals, but it will also always finish quickly.  We do 'reflexivity' last because
for goals of the form ?x = y, if we have x = y in the context, we will typically
want to use the assumption and not reflexivity *)
Ltac fast_done
:=
  solve
    [ eassumption
    | symmetry; eassumption
    | apply not_symmetry; eassumption
    | reflexivity ].
(* stdpp/tactics.v *)
Class TCFastDone (P : Prop) : Prop
:= tc_fast_done : P.
(* stdpp/tactics.v *)
(* A slightly modified version of Ssreflect's finishing tactic [done]. It
also performs [reflexivity] and uses symmetry of negated equalities. Compared
to Ssreflect's [done], it does not compute the goal's [hnf] so as to avoid
unfolding setoid equalities. Note that this tactic performs much better than
Coq's [easy] tactic as it does not perform [inversion]. *)
Ltac done
:=
  solve
  [ repeat first
    [ fast_done
    | solve [trivial]
    (* All the tactics below will introduce themselves anyway, or make no sense
       for goals of product type. So this is a good place for us to do it. *)
    | progress intros
    | solve [symmetry; trivial]
    | solve [apply not_symmetry; trivial]
    | discriminate
    | contradiction
    | split
    | match goal with H : is_Some None |- _ => destruct H as [? [=]] end
    | match goal with H : ¬_ |- _ => case H; clear H; fast_done end
    ]
  ].
(* stdpp/tactics.v *)
Ltac done_if b
:=
  match b with
  | true => done
  | false => idtac
  end.
(* stdpp/tactics.v *)
Ltac destruct_and_go H
:=
  try lazymatch type of H with
  | True => clear H
  | _ ∧ _ =>
    let H1 := fresh in
    let H2 := fresh in
    destruct H as [ H1 H2 ];
    destruct_and_go H1; destruct_and_go H2
  | Is_true (bool_decide _) =>
    apply (bool_decide_unpack _) in H;
    destruct_and_go H
  | Is_true (_ && _) =>
    apply andb_True in H;
    destruct_and_go H
  end.
(* stdpp/tactics.v *)
Ltac case_match
:=
  let H := fresh in case_match eqn:H.
(* stdpp/tactics.v *)
(* The tactic [var_eq x y] fails if [x] and [y] are unequal, and [var_neq]
does the converse. *)
Ltac var_eq x1 x2
:= match x1 with x2 => idtac | _ => fail 1 end.
(* stdpp/tactics.v *)
Ltac var_neq x1 x2
:= match x1 with x2 => fail 1 | _ => idtac end.
(* stdpp/tactics.v *)
(* The tactic [mk_evar T] returns a new evar of type [T], without affecting the
current context.

This is usually a more useful behavior than Coq's [evar], which is a
side-effecting tactic (not returning anything) that introduces a local
definition into the context that holds the evar.
Note that the obvious alternative [open_constr (_:T)] has subtly different
behavior, see std++ issue 115.

Usually, Ltacs cannot return a value and have a side-effect, but we use the
trick described at
<https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884>
to work around that: wrap the side-effect in a [match goal]. *)
Ltac mk_evar T
:=
  let T := constr:(T : Type) in
  let e := fresh in
  let _ := match goal with _ => evar (e:T) end in
  let e' := eval unfold e in e in
  let _ := match goal with _ => clear e end in
  e'.
(* stdpp/tactics.v *)
(* The tactic [get_head t] returns the head function [f] when [t] is of the
shape [f a1 ... aN]. This is purely syntactic, no unification is performed. *)
Ltac get_head e
:=
  lazymatch e with
  | ?h _ => get_head h
  | _    => e
  end.
(* stdpp/tactics.v *)
(* The tactic [no_new_unsolved_evars tac] executes [tac] and fails if it
creates any new evars or leaves behind any subgoals. *)
Ltac no_new_unsolved_evars tac
:= solve [unshelve tac].
(* stdpp/tactics.v *)
(* Operational type class projections in recursive calls are not folded back
appropriately by [simpl]. The tactic [csimpl] uses the [fold_classes] tactics
to refold recursive calls of [fmap], [mbind], [omap] and [alter]. A
self-contained example explaining the problem can be found in the following
Coq-club message:

https://sympa.inria.fr/sympa/arc/coq-club/2012-10/msg00147.html *)
Ltac fold_classes
:=
  repeat match goal with
  | |- context [ ?F ] =>
    progress match type of F with
    | FMap _ =>
       change F with (@fmap _ F);
       repeat change (@fmap _ (@fmap _ F)) with (@fmap _ F)
    | MBind _ =>
       change F with (@mbind _ F);
       repeat change (@mbind _ (@mbind _ F)) with (@mbind _ F)
    | OMap _ =>
       change F with (@omap _ F);
       repeat change (@omap _ (@omap _ F)) with (@omap _ F)
    | Alter _ _ _ =>
       change F with (@alter _ _ _ F);
       repeat change (@alter _ _ _ (@alter _ _ _ F)) with (@alter _ _ _ F)
    end
  end.
(* stdpp/tactics.v *)
Ltac fold_classes_hyps H
:=
  repeat match type of H with
  | context [ ?F ] =>
    progress match type of F with
    | FMap _ =>
       change F with (@fmap _ F) in H;
       repeat change (@fmap _ (@fmap _ F)) with (@fmap _ F) in H
    | MBind _ =>
       change F with (@mbind _ F) in H;
       repeat change (@mbind _ (@mbind _ F)) with (@mbind _ F) in H
    | OMap _ =>
       change F with (@omap _ F) in H;
       repeat change (@omap _ (@omap _ F)) with (@omap _ F) in H
    | Alter _ _ _ =>
       change F with (@alter _ _ _ F) in H;
       repeat change (@alter _ _ _ (@alter _ _ _ F)) with (@alter _ _ _ F) in H
    end
  end.
(* stdpp/tactics.v *)
Ltac setoid_subst_aux R x
:=
  match goal with
  | H : R x ?y |- _ =>
     is_var x;
     try match y with x _ => fail 2 end;
     repeat match goal with
     | |- context [ x ] => setoid_rewrite H
     | H' : context [ x ] |- _ =>
        try match H' with H => fail 2 end;
        setoid_rewrite H in H'
     end;
     clear x H
  end.
(* stdpp/tactics.v *)
Ltac setoid_subst
:=
  repeat match goal with
  | _ => progress simplify_eq/=
  | H : @equiv ?A ?e ?x _ |- _ => setoid_subst_aux (@equiv A e) x
  | H : @equiv ?A ?e _ ?x |- _ => symmetry in H; setoid_subst_aux (@equiv A e) x
  end.
(* stdpp/tactics.v *)
(* A little helper for [f_equiv] and [solve_proper] that simplifies away [flip]
relations. *)
Ltac clean_flip
:=
  repeat match goal with
  | |- (flip ?R) ?x ?y => change (R y x)
  | H : (flip ?R) ?x ?y |- _ => change (R y x) in H
  end.
(* stdpp/tactics.v *)
(* The typeclass [SolveProperSubrelation] is used by the [solve_proper] tactic
when the goal is of the form [R1 x y] and there are assumptions of the form [R2
x y]. We cannot use Coq's [subrelation] class here as adding the [subrelation]
instances causes lots of backtracking in the [Proper] hint search, resulting in
very slow/diverging [rewrite]s due to exponential instance search. *)
Class SolveProperSubrelation {A} (R R' : relation A)
:=
  is_solve_proper_subrelation x y : R x y → R' x y.
(* stdpp/tactics.v *)
Instance subrelation_solve_proper_subrelation {A} (R R' : relation A) :
  subrelation R R' →
  SolveProperSubrelation R R'.
Proof. intros ???. apply is_subrelation. Qed.
(* stdpp/tactics.v *)
(* The tactic [solve_proper_unfold] unfolds the first head symbol, so that
we proceed by repeatedly using [f_equiv]. *)
Ltac solve_proper_unfold
:=
  (* Try unfolding the head symbol, which is the one we are proving a new property about *)
  try lazymatch goal with
  | |- ?R ?t1 ?t2 =>
    let h1 := get_head t1 in
    let h2 := get_head t2 in
    unify h1 h2;
    unfold h1
  end.
(* stdpp/tactics.v *)
(* [solve_proper_prepare] does some preparation work before the main
[solve_proper] loop.  Having this as a separate tactic is useful for debugging
[solve_proper] failure. *)
Ltac solve_proper_prepare
:=
  (* Introduce everything *)
  intros;
  repeat lazymatch goal with
  | |- Proper _ _ => intros ???
  | |- (_ ==> _)%signature _ _ => intros ???
  | |- pointwise_relation _ _ _ _ => intros ?
  | |- ?R ?f _ =>
     (* Deal with other cases where we have an equivalence relation on functions
     (e.g. a [pointwise_relation] that is hidden in some form in [R]). We do
     this by checking if the arguments of the relation are actually functions,
     and then forcefully introduce one ∀ and introduce the remaining ∀s that
     show up in the goal. To check that we actually have an equivalence relation
     on functions, we try to eta expand [f], which will only succeed if [f] is
     actually a function. *)
     let f' := constr:(λ x, f x) in
     (* Now forcefully introduce the first ∀ and other ∀s that show up in the
     goal afterwards. *)
     intros ?; intros
  end;
  (* Simplify things, if we can. *)
  simplify_eq;
  (* We try with and without unfolding. We have to backtrack on
     that because unfolding may succeed, but then the proof may fail. *)
  (solve_proper_unfold + idtac); simpl.
(* stdpp/tactics.v *)
(* [solve_proper_finish] is basically a version of [eassumption]
that can also take into account [subrelation]. *)
Ltac solve_proper_finish
:=
  (* We always try this first, since the syntactic match below is not always
  able to find the assumptions we are looking for (e.g. when [Some x ⊑ Some y]
  is convertible to [x ⊑ y]). *)
  eassumption ||
  match goal with
  | H : ?R1 ?x ?y |- ?R2 ?x ?y =>
    no_new_unsolved_evars ltac:(eapply (is_solve_proper_subrelation H))
  end.
(* stdpp/tactics.v *)
(* The tactic [solve_proper_core tac] solves goals of the form "Proper (R1 ==> R2)", for
any number of relations. The actual work is done by repeatedly applying
[tac]. *)
Ltac solve_proper_core tac
:=
  solve_proper_prepare;
  (* Now do the job. The inner tactics can rely on [flip] having been cleaned. *)
  solve [repeat (clean_flip; first [solve_proper_finish | tac ()]) ].
(* stdpp/tactics.v *)
(* Finally, [solve_proper] tries to apply [f_equiv] in a loop. *)
Ltac solve_proper
:= solve_proper_core ltac:(fun _ => f_equiv).
(* stdpp/tactics.v *)
(* The tactic [intros_revert tac] introduces all foralls/arrows, performs tac,
and then reverts them. *)
Ltac intros_revert tac
:=
  lazymatch goal with
  | |- ∀ _, _ => let H := fresh in intro H; intros_revert tac; revert H
  | |- _ => tac
  end.
(* stdpp/tactics.v *)
(* Runs [tac] on the n-th hypothesis that can be introduced from the goal. *)
Ltac num_tac n tac
:=
  intros until n;
  lazymatch goal with
  (* matches the last hypothesis, which is what we want *)
  | H : _ |- _ => tac H
  end.
(* stdpp/tactics.v *)
(* The helper [opose_core p tac] takes a uconstr [p] and turns it into a constr
that is passed to [tac]. All underscores inside [p] become evars, and the ones
that are unifiable (i.e, appear in the type of other evars) are shelved.

This is similar to creating a [open_constr], except that we have control over
what does and does not get shelved. Creating a [open_constr] would shelve every
created evar, which is not what we want, and it is hard to avoid since it
happens very early (before we can easily wrap things in [unshelve]). *)
Ltac opose_core p tac
:=
  (* The "opose_internal" here is useful for debugging but not helpful for name
  collisions since it gets ignored with name mangling. The [clear] below is what
  ensures we don't get name collisions. *)
  let i := fresh "opose_internal" in
  unshelve (epose _ as i);
    [shelve (*type of [p]*)
    |refine p (* will create the subgoals, and shelve some of them *)
    |(* Now we have [i := t] in the context, let's get the [t] and remove [i]. *)
     let t := eval unfold i in i in
     (* We want to leave the context exactly as we found it, to avoid
     any issues with fresh name generation. So clear [i] before calling
     the user-visible tactic. *)
     clear i;
     tac t];
  (* [tac] might have added more subgoals, making some existing ones
  unifiable, so we need to shelve again. *)
  shelve_unifiable.