Commit 01d12014 authored by Ralf Jung's avatar Ralf Jung

let solve_inG handle higher-arity functions for the \Sigma

parent be81fb92
Pipeline #3651 passed with stage
in 10 minutes and 54 seconds
...@@ -21,8 +21,11 @@ Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed. ...@@ -21,8 +21,11 @@ Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
Ltac solve_inG := Ltac solve_inG :=
(* Get all assumptions *) (* Get all assumptions *)
intros; intros;
(* Unfold the top-level xΣ *) (* Unfold the top-level xΣ. We need to support this to be a function. *)
lazymatch goal with lazymatch goal with
| H : subG (?xΣ _ _ _ _) _ |- _ => try unfold xΣ in H
| H : subG (?xΣ _ _ _) _ |- _ => try unfold xΣ in H
| H : subG (?xΣ _ _) _ |- _ => try unfold xΣ in H
| H : subG (?xΣ _) _ |- _ => try unfold xΣ in H | H : subG (?xΣ _) _ |- _ => try unfold xΣ in H
| H : subG ?xΣ _ |- _ => try unfold xΣ in H | H : subG ?xΣ _ |- _ => try unfold xΣ in H
end; end;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment