% Mizar problem: t40_margrel1,margrel1,636,13 
fof(t40_margrel1,conjecture,(
    ! [A] : 
      ( v2_margrel1(A)
     => k9_margrel1(k9_margrel1(A)) = A ) ),
    inference(mizar_bg_added,[status(thm)],[involutiveness_k9_margrel1,dt_k9_margrel1,rc2_margrel1,fc4_margrel1]),
    [file(margrel1,t40_margrel1)]).

fof(involutiveness_k9_margrel1,axiom,(
    ! [A] : 
      ( v2_margrel1(A)
     => k9_margrel1(k9_margrel1(A)) = A ) ),
    file(margrel1,k9_margrel1),
    []).

fof(dt_k9_margrel1,axiom,(
    ! [A] : 
      ( v2_margrel1(A)
     => v2_margrel1(k9_margrel1(A)) ) ),
    file(margrel1,k9_margrel1),
    []).

fof(rc2_margrel1,axiom,(
    ? [A] : v2_margrel1(A) ),
    file(margrel1,rc2_margrel1),
    []).

fof(fc4_margrel1,axiom,(
    ! [A] : 
      ( v2_margrel1(A)
     => v2_margrel1(k9_margrel1(A)) ) ),
    file(margrel1,fc4_margrel1),
    []).