`unfold n` fails to match

[kyagrd]

lemma1 in the following Abella code in the file pp.thm, which is forall P M N, {eq M N} -> eq_struct_pp (P M) (P N), should obviously be provable because it exactly matches the structure of the second clause of eq_struct_pp predicate, which is eq_struct_pp (P M) (P N) := {eq M N}. However, I cannot find a way to do it because unfold 2 fails to do the job.

sig pp.    %%%% pp.sig 

kind nm  type.

kind tm  type.
type nm   nm -> tm.
type pr   tm -> tm -> tm.
type fst  tm -> tm.
type snd  tm -> tm.

kind pp  type. % plain process
type null  pp.
type par   pp -> pp -> pp.      % parallel comp.
type in    tm -> (tm -> pp) -> pp. 
type out   tm -> tm -> pp -> pp.

type red  tm -> tm -> o. % term reduction
type eq   tm -> tm -> o. % term equality

module pp.  %%%% pp.mod

red (fst (pr M N)) M.
red (snd (pr M N)) N.
red (pr M N) (pr M' N) :- red M M'.
red (pr M N) (pr M N') :- red N N'.
red (fst M) (fst N) :- red M N.
red (snd M) (snd N) :- red M N.

eq M M.
eq (pr M1 M2) (pr N1 N2) :- eq M1 N1, eq M2 N2.
eq (fst M) (fst N) :- eq M N.
eq (snd M) (snd N) :- eq M N.
eq M N :- red M M1, eq M1 N.
eq M N :- red N N1, eq M N1.

%%%% pp.thm %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Specification "pp". % spec of a simple value passing proc. calc. with par. comp.

Set types on.
% Set witnesses on.

% Evaluation Context Relation for processes
Define evctx_rel_pp : pp -> pp -> pp -> pp -> prop
by evctx_rel_pp P1 P2 P1 P2
;  evctx_rel_pp P1 P2 (par E1 B) (par E2 B) := evctx_rel_pp P1 P2 E1 E2
;  evctx_rel_pp P1 P2 (par B E1) (par B E2) := evctx_rel_pp P1 P2 E1 E2
.

% evaluation context for single process defined as a rel over two identical processes
Define evctx_pp : pp -> pp -> prop by evctx_pp A B := evctx_rel_pp A A B B.

% Structural Equivalence for processes
Define eq_struct_pp : pp -> pp -> prop
by eq_struct_pp P P % reflexive
;  eq_struct_pp (P M) (P N) := {eq M N}            % REWRITE  %%% trying to match with this
;  eq_struct_pp (par A (par B C)) (par (par A B) C) % PAR-A
;  eq_struct_pp (par A B) (par B A)                 % PAR-C
;  eq_struct_pp A (par A null)                      % PAR-0
;  eq_struct_pp EA EB := exists A B, eq_struct_pp A B /\ evctx_rel_pp A B EA EB % closed by evctx.
;  eq_struct_pp P Q := exists R, eq_struct_pp P R /\ eq_struct_pp R Q % transitive
;  eq_struct_pp P Q := eq_struct_pp Q P % symmetric
.

Theorem lemma1 : forall P M N, {eq M N} -> eq_struct_pp (P M) (P N).
% intros. search. %%% <== this doesn't work. so let's unfold ...
% intros. unfold. %%% unfolds to wrong clause. so let's try more fancy unfold features ...
% intros. unfold (all). right. %%% <=== dosn't work. comes back where it stareted before unfold
intros. unfold 2. %%% <=== error no mathcing clasues. Why??? in fact none of 1-8 works :(
abort.

[chaudhuri]

Unclear how this can/should be addressed. We generally do not support non-pattern heads.

Will close after a month or two unless someone has some actionable suggestions.

[chaudhuri]

I'm guessing that there won't be much progress on this any time soon. Please reopen if anyone has any bright ideas.